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	12 math math: face_mono, monotone_face, BoxIntegral.hasIntegral_GP_pderiv, BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt, face_mk, face_lower, 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	35 math math: splitCenterBox_le, BoxIntegral.TaggedPrepartition.tag_mem_Icc, upper_mem_Icc, 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, measure_Icc_lt_top, coe_ae_eq_Icc, Ioo_ae_eq_Icc, BoxIntegral.Prepartition.le_biUnionIndex, lower_mem_Icc, 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	16 math math: BoxIntegral.unitPartition.mem_box_iff', exists_mem_splitCenterBox, BoxIntegral.unitPartition.tag_mem, ext_iff, 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	17 math math: BoxIntegral.TaggedPrepartition.isHenstock_single, disjoint_withBotCoe, Ioo_subset_coe, splitUpper_le, monotone_face, 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	34 math math: le_TFAE, upper_sub_lower_splitCenterBox, BoxIntegral.hasIntegral_GP_pderiv, BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt, face_lower, le_iff_bounds, nndist_le_distortion_mul, splitUpper_eq_self, 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	59 math, 4 bridge math: BoxIntegral.Prepartition.measure_iUnion_toReal, disjoint_splitCenterBox, coe_coe, isBounded, le_TFAE, 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, 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.SimpleFunc.box_integral_eq_integral
upper 📖	CompOp	34 math math: 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, le_iff_bounds, nndist_le_distortion_mul, 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	Fin.insertNth 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 instPartialOrderNNReal 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 AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid 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 AddRightCancelSemigroup.toIsRightCancelAdd 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	—	Set Set.instHasSubset DFunLike.coe OrderEmbedding BoxIntegral.Box instLE Set.instLE instFunLikeOrderEmbedding Icc OrderHom Nat.instPreorder PartialOrder.toPreorder instPartialOrder 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 Fin.succAbove	—	—
face_mono 📖	mathematical	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 Set 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 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 DFunLike.coe OrderEmbedding BoxIntegral.Box 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 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 instPartialOrderNNReal NNDist.nndist PseudoMetricSpace.toNNDist pseudoMetricSpacePi Real Real.pseudoMetricSpace lower upper Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal 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