Basic

📁 Source: Mathlib/Analysis/BoxIntegral/Box/Basic.lean

Statistics

Metric	Count
Definitions Ioo, inf, distortion, face, instCoeTCSetForallReal, instInhabited, instLE, instLatticeWithBot, instMembershipForallReal, instPartialOrder, instSemilatticeSup, lower, mk', toSet, upper, withBotCoe, withBotToSet	17
Theorems Icc_def, Icc_eq_pi, Ioo_subset_Icc, Ioo_subset_coe, antitone_lower, biUnion_coe_eq_coe, coe_bot, coe_coe, coe_eq_pi, coe_inf, coe_inj, coe_mk', coe_ne_empty, coe_subset_Icc, coe_subset_coe, continuousOn_face_Icc, diam_Icc_le_of_distortion_le, disjoint_coe, disjoint_withBotCoe, dist_le_distortion_mul, distortion_eq_of_sub_eq_div, empty_ne_coe, exists_mem, exists_seq_mono_tendsto, ext, ext_iff, face_lower, face_mk, face_mono, face_upper, iUnion_Ioo_of_tendsto, injective_coe, isBounded, isBounded_Icc, isCompact_Icc, isSome_iff, le_TFAE, le_def, le_iff_Icc, le_iff_bounds, lower_le_upper, lower_lt_upper, lower_mem_Icc, lower_ne_upper, mapsTo_insertNth_face, mapsTo_insertNth_face_Icc, mem_coe, mem_def, mem_mk, mem_univ_Ioc, mk'_eq_bot, mk'_eq_coe, monotone_face, monotone_upper, ne_of_disjoint_coe, nndist_le_distortion_mul, nonempty_coe, not_disjoint_coe_iff_nonempty_inter, upper_mem, upper_mem_Icc, withBotCoe_inj, withBotCoe_subset_iff	62
Total	79

BoxIntegral.Box

Definitions

Name	Category	Theorems
Ioo 📖	CompOp	6 math math: Ioo_subset_coe, iUnion_Ioo_of_tendsto, Ioo_ae_eq_Icc, Ioo_subset_Icc, exists_seq_mono_tendsto, measurableSet_Ioo
distortion 📖	CompOp	11 math math: BoxIntegral.Prepartition.distortion_le_of_mem, nndist_le_distortion_mul, exists_taggedPartition_isHenstock_isSubordinate_homothetic, distortion_eq_of_sub_eq_div, BoxIntegral.TaggedPrepartition.distortion_le_of_mem, dist_le_distortion_mul, BoxIntegral.Prepartition.distortion_top, BoxIntegral.Prepartition.distortion_le_iff, BoxIntegral.TaggedPrepartition.distortion_le_iff, BoxIntegral.IntegrationParams.toFilterDistortion_neBot, BoxIntegral.TaggedPrepartition.distortion_single
face 📖	CompOp	13 math math: face_mono, monotone_face, BoxIntegral.hasIntegral_GP_pderiv, BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt, face_mk, face_lower, BoxIntegral.BoxAdditiveMap.upperSubLower_apply, continuousOn_face_Icc, volume_face_mul, mapsTo_insertNth_face, mapsTo_insertNth_face_Icc, BoxIntegral.norm_volume_sub_integral_face_upper_sub_lower_smul_le, face_upper
instCoeTCSetForallReal 📖	CompOp	—
instInhabited 📖	CompOp	—
instLE 📖	CompOp	39 math math: splitCenterBox_le, BoxIntegral.TaggedPrepartition.tag_mem_Icc, upper_mem_Icc, face_mono, measurableSet_Icc, le_TFAE, BoxIntegral.Prepartition.le_of_mem, BoxIntegral.unitPartition.mem_admissibleIndex_iff, le_iff_Icc, BoxIntegral.Prepartition.card_filter_mem_Icc_le, isCompact_Icc, le_iff_bounds, BoxIntegral.TaggedPrepartition.isSubordinate_single, measure_Icc_lt_top, coe_ae_eq_Icc, Ioo_ae_eq_Icc, BoxIntegral.Prepartition.le_biUnionIndex, continuousOn_face_Icc, lower_mem_Icc, BoxIntegral.TaggedPrepartition.isHenstock_single_iff, Icc_def, isBounded_Icc, BoxIntegral.Prepartition.IsPartition.le_iff, mapsTo_insertNth_face_Icc, le_def, Ioo_subset_Icc, exists_seq_mono_tendsto, diam_Icc_le_of_distortion_le, BoxIntegral.Prepartition.injOn_setOf_mem_Icc_setOf_lower_eq, BoxIntegral.TaggedPrepartition.IsSubordinate.diam_le, BoxIntegral.Prepartition.le_iff_nonempty_imp_le_and_iUnion_subset, Icc_eq_pi, coe_subset_Icc, BoxIntegral.Prepartition.le_of_mem', coe_subset_coe, BoxIntegral.Prepartition.not_disjoint_imp_le_of_subset_of_mem_splitMany, BoxIntegral.unitPartition.diam_boxIcc, BoxIntegral.Prepartition.biUnionIndex_le, BoxIntegral.Prepartition.le_def
instLatticeWithBot 📖	CompOp	—
instMembershipForallReal 📖	CompOp	17 math math: BoxIntegral.unitPartition.mem_box_iff', exists_mem_splitCenterBox, BoxIntegral.unitPartition.tag_mem, ext_iff, BoxIntegral.Prepartition.IsPartition.existsUnique, BoxIntegral.unitPartition.mem_box_iff, BoxIntegral.TaggedPrepartition.mem_iUnion, mem_splitCenterBox, mem_mk, mem_coe, le_def, mem_def, BoxIntegral.unitPartition.mem_box_iff_index, exists_mem, upper_mem, mem_univ_Ioc, BoxIntegral.Prepartition.mem_iUnion
instPartialOrder 📖	CompOp	18 math math: BoxIntegral.TaggedPrepartition.isHenstock_single, disjoint_withBotCoe, Ioo_subset_coe, splitUpper_le, monotone_face, iUnion_Ioo_of_tendsto, splitLower_le, Ioo_ae_eq_Icc, not_disjoint_coe_iff_nonempty_inter, monotone_upper, disjoint_splitLower_splitUpper, Ioo_subset_Icc, exists_seq_mono_tendsto, withBotCoe_subset_iff, disjoint_coe, measurableSet_Ioo, antitone_lower, BoxIntegral.TaggedPrepartition.isPartition_single
instSemilatticeSup 📖	CompOp	—
lower 📖	CompOp	37 math math: splitLower_def, le_TFAE, upper_sub_lower_splitCenterBox, BoxIntegral.hasIntegral_GP_pderiv, BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt, face_lower, splitUpper_def, le_iff_bounds, nndist_le_distortion_mul, splitUpper_eq_self, BoxIntegral.BoxAdditiveMap.upperSubLower_apply, BoxIntegral.BoxAdditiveMap.volume_apply, exists_taggedPartition_isHenstock_isSubordinate_homothetic, dist_le_distortion_mul, mem_splitCenterBox, volume_face_mul, lower_mem_Icc, volume_apply', BoxIntegral.unitPartition.box_lower, Icc_def, splitLower_eq_bot, exists_seq_mono_tendsto, mk'_eq_coe, diam_Icc_le_of_distortion_le, BoxIntegral.norm_volume_sub_integral_face_upper_sub_lower_smul_le, BoxIntegral.Prepartition.injOn_setOf_mem_Icc_setOf_lower_eq, lower_le_upper, mem_def, Icc_eq_pi, BoxIntegral.Prepartition.upper_sub_lower_of_mem_splitCenter, coe_eq_pi, volume_apply, lower_lt_upper, BoxIntegral.unitPartition.box.upper_sub_lower, mem_univ_Ioc, antitone_lower, BoxIntegral.Prepartition.lower_le_lower
mk' 📖	CompOp	3 math math: coe_mk', mk'_eq_bot, mk'_eq_coe
toSet 📖	CompOp	61 math, 5 bridge math: BoxIntegral.Prepartition.measure_iUnion_toReal, disjoint_splitCenterBox, coe_coe, isBounded, le_TFAE, BoxIntegral.Prepartition.isPartitionDisjUnionOfEqDiff, measurableSet_coe, Ioo_subset_coe, coe_inj, BoxIntegral.Prepartition.subset_iUnion, BoxIntegral.Prepartition.exists_iUnion_eq_diff, BoxIntegral.Prepartition.IsPartition.iUnion_eq, BoxIntegral.Prepartition.mem_split_iff', BoxIntegral.Prepartition.iUnion_def, measure_coe_lt_top, MeasureTheory.AEContinuous.hasBoxIntegral, BoxIntegral.Prepartition.mem_restrict', BoxIntegral.Prepartition.iUnion_subset, coe_ae_eq_Icc, BoxIntegral.TaggedPrepartition.iUnion_unionComplToSubordinate_boxes, nonempty_coe, BoxIntegral.unitPartition.disjoint, BoxIntegral.Prepartition.exists_splitMany_inf_eq_filter_of_finite, mem_coe, volume_apply', BoxIntegral.norm_integral_le_of_le_const, not_disjoint_coe_iff_nonempty_inter, BoxIntegral.Prepartition.iUnion_top, biUnion_coe_eq_coe, BoxIntegral.Prepartition.pairwiseDisjoint, BoxIntegral.unitPartition.setFinite_index, BoxIntegral.Prepartition.iUnion_compl, mapsTo_insertNth_face, BoxIntegral.TaggedPrepartition.subset_iUnion, BoxIntegral.le_hasIntegralVertices_of_isBounded, coe_splitLower, BoxIntegral.TaggedPrepartition.iUnion_subset, MeasureTheory.ContinuousOn.hasBoxIntegral, iUnion_coe_splitCenterBox, disjoint_coe, BoxIntegral.TaggedPrepartition.iUnion_single, BoxIntegral.Prepartition.coe_eq_of_mem_split_of_mem_le, BoxIntegral.Prepartition.iUnion_def', BoxIntegral.Prepartition.iUnion_splitMany, MeasureTheory.Measure.toBoxAdditive_apply, BoxIntegral.Prepartition.iUnion_restrict, BoxIntegral.Prepartition.isPartition_iff_iUnion_eq, BoxIntegral.TaggedPrepartition.isPartition_iff_iUnion_eq, coe_subset_Icc, coe_eq_pi, BoxIntegral.Prepartition.coe_eq_of_mem_split_of_lt_mem, BoxIntegral.TaggedPrepartition.iUnion_def, BoxIntegral.unitPartition.volume_box, BoxIntegral.Prepartition.disjoint_coe_of_mem, coe_subset_coe, BoxIntegral.Prepartition.eventually_splitMany_inf_eq_filter, coe_splitUpper, BoxIntegral.IntegrationParams.MemBaseSet.exists_common_compl, injective_coe, BoxIntegral.Prepartition.iUnion_split, BoxIntegral.Prepartition.iUnion_single bridge: BoxIntegral.hasIntegralIndicatorConst, BoxIntegral.IntegrationParams.MemBaseSet.exists_compl, MeasureTheory.SimpleFunc.hasBoxIntegral, MeasureTheory.IntegrableOn.hasBoxIntegral, MeasureTheory.SimpleFunc.box_integral_eq_integral
upper 📖	CompOp	37 math math: splitLower_def, splitUpper_eq_bot, upper_mem_Icc, BoxIntegral.unitPartition.box_upper, le_TFAE, upper_sub_lower_splitCenterBox, BoxIntegral.hasIntegral_GP_pderiv, BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt, splitUpper_def, le_iff_bounds, nndist_le_distortion_mul, BoxIntegral.BoxAdditiveMap.upperSubLower_apply, BoxIntegral.BoxAdditiveMap.volume_apply, exists_taggedPartition_isHenstock_isSubordinate_homothetic, dist_le_distortion_mul, mem_splitCenterBox, volume_face_mul, volume_apply', BoxIntegral.Prepartition.upper_le_upper, Icc_def, monotone_upper, exists_seq_mono_tendsto, mk'_eq_coe, diam_Icc_le_of_distortion_le, BoxIntegral.norm_volume_sub_integral_face_upper_sub_lower_smul_le, face_upper, lower_le_upper, mem_def, Icc_eq_pi, BoxIntegral.Prepartition.upper_sub_lower_of_mem_splitCenter, coe_eq_pi, volume_apply, lower_lt_upper, splitLower_eq_self, BoxIntegral.unitPartition.box.upper_sub_lower, upper_mem, mem_univ_Ioc
withBotCoe 📖	CompOp	—
withBotToSet 📖	CompOp	12 math math: coe_coe, coe_bot, disjoint_withBotCoe, coe_mk', isSome_iff, biUnion_coe_eq_coe, coe_inf, coe_splitLower, withBotCoe_subset_iff, withBotCoe_inj, BoxIntegral.Prepartition.iUnion_ofWithBot, coe_splitUpper

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Icc_def 📖	mathematical	—	DFunLike.coe OrderEmbedding BoxIntegral.Box Set instLE Set.instLE instFunLikeOrderEmbedding Icc Set.Icc Pi.preorder Real Real.instPreorder lower upper	—	—
Icc_eq_pi 📖	mathematical	—	DFunLike.coe OrderEmbedding BoxIntegral.Box Set instLE Set.instLE instFunLikeOrderEmbedding Icc Set.pi Real Set.univ Set.Icc Real.instPreorder lower upper	—	Set.pi_univ_Icc
Ioo_subset_Icc 📖	mathematical	—	Set Set.instHasSubset DFunLike.coe OrderHom BoxIntegral.Box PartialOrder.toPreorder instPartialOrder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra OrderHom.instFunLike Ioo OrderEmbedding instLE Set.instLE instFunLikeOrderEmbedding Icc	—	HasSubset.Subset.trans Set.instIsTransSubset Ioo_subset_coe coe_subset_Icc
Ioo_subset_coe 📖	mathematical	—	Set Set.instHasSubset DFunLike.coe OrderHom BoxIntegral.Box PartialOrder.toPreorder instPartialOrder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra OrderHom.instFunLike Ioo toSet	—	Set.Ioo_subset_Ioc_self
antitone_lower 📖	mathematical	—	Antitone BoxIntegral.Box PartialOrder.toPreorder instPartialOrder Pi.preorder Real Real.instPreorder lower	—	le_iff_bounds
biUnion_coe_eq_coe 📖	mathematical	—	Set.iUnion BoxIntegral.Box WithBot WithBot.some toSet withBotToSet	—	Set.iUnion_congr_Prop Set.iUnion_of_empty instIsEmptyFalse Set.iUnion_empty Set.iUnion_iUnion_eq_left
coe_bot 📖	mathematical	—	withBotToSet Bot.bot WithBot BoxIntegral.Box WithBot.bot Set Set.instEmptyCollection	—	—
coe_coe 📖	mathematical	—	withBotToSet WithBot.some BoxIntegral.Box toSet	—	—
coe_eq_pi 📖	mathematical	—	toSet Set.pi Real Set.univ Set.Ioc Real.instPreorder lower upper	—	Set.ext mem_univ_Ioc
coe_inf 📖	mathematical	—	withBotToSet WithBot BoxIntegral.Box WithBot.inf Set Set.instInter	—	Set.empty_inter Set.inter_empty coe_mk' coe_eq_pi Set.Ioc_inter_Ioc
coe_inj 📖	mathematical	—	toSet	—	injective_coe
coe_mk' 📖	mathematical	—	withBotToSet mk' Set.pi Real Set.univ Set.Ioc Real.instPreorder	—	mk'.eq_1 coe_eq_pi coe_bot Set.univ_pi_eq_empty Set.Ioc_eq_empty
coe_ne_empty 📖	—	—	—	—	Set.Nonempty.ne_empty nonempty_coe
coe_subset_Icc 📖	mathematical	—	Set Set.instHasSubset toSet DFunLike.coe OrderEmbedding BoxIntegral.Box instLE Set.instLE instFunLikeOrderEmbedding Icc	—	LT.lt.le
coe_subset_coe 📖	mathematical	—	Set Set.instHasSubset toSet BoxIntegral.Box instLE	—	—
continuousOn_face_Icc 📖	mathematical	ContinuousOn Pi.topologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe OrderEmbedding BoxIntegral.Box Set instLE Set.instLE instFunLikeOrderEmbedding Icc Set.instMembership Set.Icc Real.instPreorder lower upper	ContinuousOn Pi.topologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Fin.insertNth DFunLike.coe OrderEmbedding BoxIntegral.Box Set instLE Set.instLE instFunLikeOrderEmbedding Icc face	—	ContinuousOn.comp ContinuousOn.finInsertNth continuousOn_const continuousOn_id mapsTo_insertNth_face_Icc
diam_Icc_le_of_distortion_le 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder distortion	Real Real.instLE Metric.diam pseudoMetricSpacePi Real.pseudoMetricSpace DFunLike.coe OrderEmbedding BoxIntegral.Box Set instLE Set.instLE instFunLikeOrderEmbedding Icc Real.instMul NNReal.toReal Real.instSub upper lower	—	mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing NNReal.coe_nonneg sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid lower_le_upper Metric.diam_le_of_forall_dist_le Real.dist_le_of_mem_pi_Icc dist_le_distortion_mul mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono
disjoint_coe 📖	mathematical	—	Disjoint WithBot BoxIntegral.Box WithBot.instPartialOrder instPartialOrder WithBot.instOrderBot Preorder.toLE PartialOrder.toPreorder WithBot.some Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice toSet	—	disjoint_withBotCoe
disjoint_withBotCoe 📖	mathematical	—	Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice withBotToSet WithBot BoxIntegral.Box WithBot.instPartialOrder instPartialOrder WithBot.instOrderBot Preorder.toLE PartialOrder.toPreorder	—	coe_inf
dist_le_distortion_mul 📖	mathematical	—	Real Real.instLE Dist.dist PseudoMetricSpace.toDist pseudoMetricSpacePi Real.pseudoMetricSpace lower upper Real.instMul NNReal.toReal distortion Real.instSub	—	sub_neg IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add lower_lt_upper abs_of_neg neg_sub nndist_le_distortion_mul
distortion_eq_of_sub_eq_div 📖	mathematical	Real Real.instSub upper lower DivInvMonoid.toDiv Real.instDivInvMonoid	distortion	—	Real.nndist_eq' map_div₀ MonoidWithZeroHom.monoidWithZeroHomClass NNReal.eq div_nonpos_of_nonneg_of_nonpos IsOrderedRing.toPosMulMono Real.instIsOrderedRing sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid lower_le_upper not_lt LE.le.not_gt sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le lower_lt_upper map_ne_zero LT.lt.ne' NNReal.finset_sup_div div_div_div_cancel_right₀
empty_ne_coe 📖	—	—	—	—	coe_ne_empty
exists_mem 📖	mathematical	—	BoxIntegral.Box instMembershipForallReal	—	upper_mem
exists_seq_mono_tendsto 📖	mathematical	—	OrderHom BoxIntegral.Box Nat.instPreorder PartialOrder.toPreorder instPartialOrder Set Set.instHasSubset DFunLike.coe OrderEmbedding instLE Set.instLE instFunLikeOrderEmbedding Icc OrderHom.instFunLike ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Ioo Filter.Tendsto lower Filter.atTop nhds Pi.topologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace upper	—	le_iff_bounds StrictAnti.antitone StrictMono.monotone LT.lt.trans_le LE.le.trans_lt tendsto_pi_nhds exists_seq_strictAnti_strictMono_tendsto instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology UniformSpace.pseudoMetrizableSpace EMetric.instIsCountablyGeneratedUniformity lower_lt_upper
ext 📖	—	BoxIntegral.Box instMembershipForallReal	—	—	injective_coe Set.ext
ext_iff 📖	mathematical	—	BoxIntegral.Box instMembershipForallReal	—	ext
face_lower 📖	mathematical	—	lower face Fin.succAbove	—	—
face_mk 📖	mathematical	Real Real.instLT	face Real Fin.succAbove	—	—
face_mono 📖	mathematical	BoxIntegral.Box instLE	BoxIntegral.Box instLE face	—	Set.Ioc_subset_Ioc le_iff_bounds
face_upper 📖	mathematical	—	upper face Fin.succAbove	—	—
iUnion_Ioo_of_tendsto 📖	mathematical	Monotone BoxIntegral.Box Nat.instPreorder PartialOrder.toPreorder instPartialOrder Filter.Tendsto lower Filter.atTop nhds Pi.topologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace upper	Set.iUnion DFunLike.coe OrderHom BoxIntegral.Box Set PartialOrder.toPreorder instPartialOrder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra OrderHom.instFunLike Ioo	—	Monotone.comp_antitone Function.monotone_eval Antitone.comp_monotone antitone_lower Monotone.comp monotone_upper Set.iUnion_univ_pi_of_monotone Antitone.Ioo Set.pi_congr iUnion_Ioo_of_mono_of_isGLB_of_isLUB isGLB_of_tendsto_atTop OrderTopology.to_orderClosedTopology instOrderTopologyReal instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_pi_nhds isLUB_of_tendsto_atTop
injective_coe 📖	mathematical	—	BoxIntegral.Box Set toSet	—	le_antisymm
isBounded 📖	mathematical	—	Bornology.IsBounded Pi.instBornology Real PseudoMetricSpace.toBornology Real.pseudoMetricSpace toSet	—	Bornology.IsBounded.subset isBounded_Icc coe_subset_Icc
isBounded_Icc 📖	mathematical	—	Bornology.IsBounded Pi.instBornology Real PseudoMetricSpace.toBornology Real.pseudoMetricSpace DFunLike.coe OrderEmbedding BoxIntegral.Box Set instLE Set.instLE instFunLikeOrderEmbedding Icc	—	nonempty_fintype Metric.isBounded_Icc Pi.compact_Icc_space' ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal
isCompact_Icc 📖	mathematical	—	IsCompact Pi.topologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe OrderEmbedding BoxIntegral.Box Set instLE Set.instLE instFunLikeOrderEmbedding Icc	—	CompactIccSpace.isCompact_Icc Pi.compact_Icc_space' ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal
isSome_iff 📖	mathematical	—	BoxIntegral.Box Set.Nonempty withBotToSet	—	nonempty_coe
le_TFAE 📖	mathematical	—	List.TFAE BoxIntegral.Box instLE Set Set.instHasSubset toSet Set.Icc Pi.preorder Real Real.instPreorder lower upper Pi.hasLe Real.instLE	—	coe_eq_pi closure_pi_set closure_Ioc instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Set.pi_univ_Icc closure_mono Set.Icc_subset_Icc_iff lower_le_upper Set.Ioc_subset_Ioc List.tfae_of_cycle
le_def 📖	mathematical	—	BoxIntegral.Box instLE instMembershipForallReal	—	—
le_iff_Icc 📖	mathematical	—	BoxIntegral.Box instLE Set Set.instHasSubset DFunLike.coe OrderEmbedding Set.instLE instFunLikeOrderEmbedding Icc	—	List.TFAE.out le_TFAE
le_iff_bounds 📖	mathematical	—	BoxIntegral.Box instLE Pi.hasLe Real Real.instLE lower upper	—	List.TFAE.out le_TFAE
lower_le_upper 📖	mathematical	—	Pi.hasLe Real Real.instLE lower upper	—	LT.lt.le lower_lt_upper
lower_lt_upper 📖	mathematical	—	Real Real.instLT lower upper	—	—
lower_mem_Icc 📖	mathematical	—	Set Set.instMembership DFunLike.coe OrderEmbedding BoxIntegral.Box instLE Set.instLE instFunLikeOrderEmbedding Icc lower	—	Set.left_mem_Icc lower_le_upper
lower_ne_upper 📖	—	—	—	—	LT.lt.ne lower_lt_upper
mapsTo_insertNth_face 📖	mathematical	Real Set Set.instMembership Set.Ioc Real.instPreorder lower upper	Set.MapsTo Fin.insertNth Real toSet face	—	Fin.forall_iff_succAbove Fin.insertNth_apply_same Fin.insertNth_apply_succAbove
mapsTo_insertNth_face_Icc 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder lower upper	Set.MapsTo Fin.insertNth Real DFunLike.coe OrderEmbedding BoxIntegral.Box Set instLE Set.instLE instFunLikeOrderEmbedding Icc face	—	Fin.insertNth_mem_Icc
mem_coe 📖	mathematical	—	Set Set.instMembership toSet BoxIntegral.Box instMembershipForallReal	—	—
mem_def 📖	mathematical	—	BoxIntegral.Box instMembershipForallReal Real Set Set.instMembership Set.Ioc Real.instPreorder lower upper	—	—
mem_mk 📖	mathematical	Real Real.instLT	BoxIntegral.Box instMembershipForallReal Real Set Set.instMembership Set.Ioc Real.instPreorder	—	—
mem_univ_Ioc 📖	mathematical	—	Set Set.instMembership Set.pi Real Set.univ Set.Ioc Real.instPreorder lower upper BoxIntegral.Box instMembershipForallReal	—	Set.mem_univ_pi
mk'_eq_bot 📖	mathematical	—	mk' Bot.bot WithBot BoxIntegral.Box WithBot.bot Real Real.instLE	—	mk'.eq_1
mk'_eq_coe 📖	mathematical	—	mk' WithBot.some BoxIntegral.Box lower upper	—	mk'.eq_1
monotone_face 📖	mathematical	—	Monotone BoxIntegral.Box PartialOrder.toPreorder instPartialOrder face	—	face_mono
monotone_upper 📖	mathematical	—	Monotone BoxIntegral.Box PartialOrder.toPreorder instPartialOrder Pi.preorder Real Real.instPreorder upper	—	le_iff_bounds
ne_of_disjoint_coe 📖	—	Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice toSet	—	—	Disjoint.ne coe_ne_empty
nndist_le_distortion_mul 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder NNDist.nndist PseudoMetricSpace.toNNDist pseudoMetricSpacePi Real Real.pseudoMetricSpace lower upper Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring distortion	—	div_mul_cancel₀ nndist_eq_zero LT.lt.ne lower_lt_upper distortion.eq_1 le_imp_le_of_le_of_le le_refl mul_le_mul_left covariant_swap_mul_of_covariant_mul NNReal.mulLeftMono Finset.le_sup Finset.mem_univ
nonempty_coe 📖	mathematical	—	Set.Nonempty toSet	—	exists_mem
not_disjoint_coe_iff_nonempty_inter 📖	mathematical	—	Disjoint WithBot BoxIntegral.Box WithBot.instPartialOrder instPartialOrder WithBot.instOrderBot Preorder.toLE PartialOrder.toPreorder WithBot.some Set.Nonempty Set Set.instInter toSet	—	disjoint_coe Set.not_disjoint_iff_nonempty_inter
upper_mem 📖	mathematical	—	BoxIntegral.Box instMembershipForallReal upper	—	Set.right_mem_Ioc lower_lt_upper
upper_mem_Icc 📖	mathematical	—	Set Set.instMembership DFunLike.coe OrderEmbedding BoxIntegral.Box instLE Set.instLE instFunLikeOrderEmbedding Icc upper	—	Set.right_mem_Icc lower_le_upper
withBotCoe_inj 📖	mathematical	—	withBotToSet	—	—
withBotCoe_subset_iff 📖	mathematical	—	Set Set.instHasSubset withBotToSet WithBot BoxIntegral.Box Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder instPartialOrder	—	—

BoxIntegral.Box.WithBot

Definitions

Name	Category	Theorems
inf 📖	CompOp	3 math math: BoxIntegral.Box.coe_inf, BoxIntegral.Prepartition.mem_inf, BoxIntegral.Prepartition.mem_restrict

---

← Back to Index