Basic

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

Statistics

Metric	Count
Definitions Prepartition, IsPartition, biUnion, biUnionIndex, boxes, disjUnion, distortion, filter, iUnion, instInhabited, instLE, instMembershipBox, instOrderBot, instOrderTop, instSemilatticeInf, ofWithBot, partialOrder, restrict, single	19
Theorems biUnion, eq_of_boxes_subset, existsUnique, iUnion_eq, iUnion_subset, inf, le_iff, nonempty_boxes, restrict, biUnionIndex_le, biUnionIndex_mem, biUnionIndex_of_mem, biUnion_assoc, biUnion_boxes, biUnion_congr, biUnion_congr_of_le, biUnion_le, biUnion_le_iff, biUnion_top, bot_boxes, card_filter_mem_Icc_le, disjUnion_boxes, disjoint_boxes_of_disjoint_iUnion, disjoint_coe_of_mem, distortion_biUnion, distortion_bot, distortion_disjUnion, distortion_le_iff, distortion_le_of_mem, distortion_of_const, distortion_top, eq_of_boxes_subset_iUnion_superset, eq_of_le, eq_of_le_of_le, eq_of_mem_of_mem, ext, ext_iff, filter_boxes, filter_le, filter_of_true, filter_true, iUnion_biUnion, iUnion_biUnion_partition, iUnion_bot, iUnion_def, iUnion_def', iUnion_disjUnion, iUnion_eq_empty, iUnion_filter_not, iUnion_inf, iUnion_mono, iUnion_ofWithBot, iUnion_restrict, iUnion_single, iUnion_subset, iUnion_top, inf_def, injOn_setOf_mem_Icc_setOf_lower_eq, injective_boxes, isPartitionDisjUnionOfEqDiff, isPartitionTop, isPartition_iff_iUnion_eq, isPartition_single_iff, le_biUnionIndex, le_biUnion_iff, le_def, le_iff_nonempty_imp_le_and_iUnion_subset, le_ofWithBot, le_of_mem, le_of_mem', lower_le_lower, mem_biUnion, mem_biUnionIndex, mem_boxes, mem_disjUnion, mem_filter, mem_iUnion, mem_inf, mem_mk, mem_ofWithBot, mem_restrict, mem_restrict', mem_single, mem_top, monotone_restrict, notMem_bot, ofWithBot_le, ofWithBot_mono, pairwiseDisjoint, restrict_biUnion, restrict_boxes_of_le, restrict_mono, restrict_self, single_boxes, subset_iUnion, sum_biUnion_boxes, sum_disj_union_boxes, sum_fiberwise, sum_ofWithBot, top_boxes, upper_le_upper	101
Total	120

BoxIntegral

Definitions

Name	Category	Theorems
Prepartition 📖	CompData	69 math math: Prepartition.biUnion_le_iff, IntegrationParams.tendsto_embedBox_toFilteriUnion_top, Prepartition.le_ofWithBot, Prepartition.mem_split_iff, Prepartition.top_boxes, HasIntegral.tendsto, Prepartition.IsPartition.compl_eq_bot, Prepartition.injective_boxes, IntegrationParams.eventually_isPartition, Prepartition.IsPartition.existsUnique, TaggedPrepartition.mem_toPrepartition, Prepartition.mem_split_iff', Prepartition.mem_biUnion, Prepartition.isPartitionTop, TaggedPrepartition.mem_mk, Prepartition.iUnion_def, IntegrationParams.hasBasis_toFilteriUnion_top, Prepartition.compl_top, Prepartition.mem_single, Prepartition.mem_restrict', Prepartition.mem_mk, Prepartition.biUnion_top, Prepartition.bot_boxes, Prepartition.mem_filter, Prepartition.iUnion_inf, Prepartition.mem_splitCenter, Prepartition.iUnion_eq_empty, Prepartition.biUnion_le, Prepartition.inf_split, Prepartition.exists_splitMany_inf_eq_filter_of_finite, Prepartition.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq, Prepartition.iUnion_top, Prepartition.distortion_top, Prepartition.iUnion_biUnion, Prepartition.iUnion_bot, Prepartition.IsPartition.le_iff, Prepartition.IsPartition.inf, Prepartition.splitMany_empty, Prepartition.iUnion_biUnionTagged, Prepartition.splitMany_insert, Prepartition.distortion_bot, Prepartition.injOn_setOf_mem_Icc_setOf_lower_eq, Prepartition.splitMany_le_split, Prepartition.monotone_restrict, Prepartition.le_iff_nonempty_imp_le_and_iUnion_subset, integralSum_sub_partitions, Prepartition.mem_boxes, integrable_iff_cauchy, Prepartition.mem_ofWithBot, Prepartition.split_of_notMem_Ioo, Prepartition.toSubordinate_toPrepartition_le, Prepartition.mem_inf, Prepartition.inf_def, Prepartition.inf_splitMany, Prepartition.mem_restrict, Prepartition.le_biUnion_iff, Prepartition.filter_le, Prepartition.IsPartition.exists_splitMany_le, Prepartition.notMem_bot, Prepartition.mem_biUnionTagged, Prepartition.ofWithBot_mono, Prepartition.eventually_splitMany_inf_eq_filter, TaggedPrepartition.infPrepartition_toPrepartition, IntegrationParams.exists_memBaseSet_le_iUnion_eq, Prepartition.ext_iff, Prepartition.mem_top, Prepartition.le_def, Prepartition.mem_disjUnion, Prepartition.mem_iUnion

BoxIntegral.Prepartition

Definitions

Name	Category	Theorems
IsPartition 📖	MathDef	7 math math: isPartitionDisjUnionOfEqDiff, isPartitionTop, isPartition_iff_iUnion_eq, isPartition_single_iff, isPartitionSplit, isPartition_splitMany, isPartition_splitCenter
biUnion 📖	CompOp	17 math math: biUnion_le_iff, biUnion_assoc, restrict_biUnion, mem_biUnion, biUnion_congr, biUnion_top, biUnion_le, inf_split, IsPartition.biUnion, iUnion_biUnion, biUnion_boxes, distortion_biUnion, inf_def, inf_splitMany, le_biUnion_iff, iUnion_biUnion_partition, biUnion_congr_of_le
biUnionIndex 📖	CompOp	7 math math: biUnion_assoc, biUnionIndex_mem, le_biUnionIndex, BoxIntegral.TaggedPrepartition.biUnionPrepartition_tag, biUnionIndex_of_mem, mem_biUnionIndex, biUnionIndex_le
boxes 📖	CompOp	39 math math: measure_iUnion_toReal, BoxIntegral.TaggedPrepartition.filter_boxes_val, BoxIntegral.unitPartition.mem_prepartition_boxes_iff, top_boxes, card_filter_mem_Icc_le, injective_boxes, filter_boxes, sum_fiberwise, sum_biUnion_boxes, bot_boxes, BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet, distortion_biUnionTagged, BoxIntegral.Integrable.sum_integral_congr, BoxIntegral.integralSum_biUnionTagged, pairwiseDisjoint, sum_disj_union_boxes, BoxIntegral.integralSum_fiberwise, BoxIntegral.TaggedPrepartition.distortion_biUnionPrepartition, biUnion_boxes, BoxIntegral.BoxAdditiveMap.sum_partition_boxes, distortion_biUnion, IsPartition.nonempty_boxes, single_boxes, BoxIntegral.TaggedPrepartition.IsHenstock.card_filter_tag_eq_le, disjUnion_boxes, BoxIntegral.integralSum_sub_partitions, iUnion_def', mem_boxes, BoxIntegral.TaggedPrepartition.disjUnion_boxes, BoxIntegral.TaggedPrepartition.single_boxes_val, BoxIntegral.TaggedPrepartition.unionComplToSubordinate_boxes, disjoint_boxes_of_disjoint_iUnion, BoxIntegral.Integrable.tendsto_integralSum_sum_integral, sum_split_boxes, BoxIntegral.BoxAdditiveMap.sum_partition_boxes', restrict_boxes_of_le, BoxIntegral.BoxAdditiveMap.sum_boxes_congr, BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq, sum_ofWithBot
disjUnion 📖	CompOp	5 math math: isPartitionDisjUnionOfEqDiff, iUnion_disjUnion, distortion_disjUnion, disjUnion_boxes, mem_disjUnion
distortion 📖	CompOp	13 math, 1 bridge math: BoxIntegral.IntegrationParams.toFilterDistortioniUnion_neBot', distortion_le_of_mem, exists_tagged_le_isHenstock_isSubordinate_iUnion_eq, distortion_top, BoxIntegral.TaggedPrepartition.distortion_biUnionPrepartition, distortion_disjUnion, distortion_biUnion, distortion_of_const, distortion_bot, distortion_le_iff, BoxIntegral.TaggedPrepartition.distortion_unionComplToSubordinate, BoxIntegral.IntegrationParams.MemBaseSet.exists_common_compl, distortion_toSubordinate bridge: BoxIntegral.IntegrationParams.MemBaseSet.exists_compl
filter 📖	CompOp	9 math math: filter_boxes, sum_fiberwise, mem_filter, exists_splitMany_inf_eq_filter_of_finite, iUnion_filter_not, filter_of_true, filter_true, filter_le, eventually_splitMany_inf_eq_filter
iUnion 📖	CompOp	36 math, 1 bridge math: measure_iUnion_toReal, BoxIntegral.IntegrationParams.toFilter_inf_iUnion_eq, subset_iUnion, exists_iUnion_eq_diff, IsPartition.iUnion_eq, iUnion_def, BoxIntegral.IntegrationParams.hasBasis_toFilteriUnion, iUnion_subset, iUnion_inf, iUnion_eq_empty, exists_splitMany_inf_eq_filter_of_finite, iUnion_filter_not, exists_tagged_le_isHenstock_isSubordinate_iUnion_eq, iUnion_top, iUnion_biUnion, iUnion_bot, iUnion_compl, BoxIntegral.TaggedPrepartition.iUnion_mk, iUnion_mono, le_iff_nonempty_imp_le_and_iUnion_subset, iUnion_def', iUnion_splitMany, iUnion_restrict, isPartition_iff_iUnion_eq, IsPartition.iUnion_subset, BoxIntegral.IntegrationParams.hasBasis_toFilterDistortioniUnion, iUnion_ofWithBot, iUnion_toSubordinate, eventually_splitMany_inf_eq_filter, BoxIntegral.IntegrationParams.MemBaseSet.exists_common_compl, BoxIntegral.IntegrationParams.exists_memBaseSet_le_iUnion_eq, iUnion_biUnion_partition, BoxIntegral.TaggedPrepartition.iUnion_toPrepartition, iUnion_split, mem_iUnion, iUnion_single bridge: BoxIntegral.IntegrationParams.MemBaseSet.exists_compl
instInhabited 📖	CompOp	—
instLE 📖	CompOp	35 math math: biUnion_le_iff, BoxIntegral.IntegrationParams.tendsto_embedBox_toFilteriUnion_top, le_ofWithBot, top_boxes, BoxIntegral.HasIntegral.tendsto, IsPartition.compl_eq_bot, BoxIntegral.IntegrationParams.eventually_isPartition, isPartitionTop, BoxIntegral.IntegrationParams.hasBasis_toFilteriUnion_top, compl_top, biUnion_top, bot_boxes, iUnion_eq_empty, biUnion_le, exists_tagged_le_isHenstock_isSubordinate_iUnion_eq, iUnion_top, distortion_top, iUnion_bot, IsPartition.le_iff, ofWithBot_le, splitMany_empty, distortion_bot, splitMany_le_split, le_iff_nonempty_imp_le_and_iUnion_subset, BoxIntegral.integrable_iff_cauchy, split_of_notMem_Ioo, toSubordinate_toPrepartition_le, le_biUnion_iff, filter_le, IsPartition.exists_splitMany_le, notMem_bot, ofWithBot_mono, BoxIntegral.IntegrationParams.exists_memBaseSet_le_iUnion_eq, mem_top, le_def
instMembershipBox 📖	CompOp	26 math math: mem_split_iff, IsPartition.existsUnique, BoxIntegral.TaggedPrepartition.mem_toPrepartition, mem_split_iff', mem_biUnion, BoxIntegral.TaggedPrepartition.mem_mk, iUnion_def, mem_single, mem_restrict', mem_mk, mem_filter, mem_splitCenter, iUnion_biUnion, iUnion_biUnionTagged, injOn_setOf_mem_Icc_setOf_lower_eq, mem_boxes, mem_ofWithBot, mem_inf, mem_restrict, notMem_bot, mem_biUnionTagged, ext_iff, mem_top, le_def, mem_disjUnion, mem_iUnion
instOrderBot 📖	CompOp	7 math math: IsPartition.compl_eq_bot, compl_top, bot_boxes, iUnion_eq_empty, iUnion_bot, distortion_bot, notMem_bot
instOrderTop 📖	CompOp	14 math math: BoxIntegral.IntegrationParams.tendsto_embedBox_toFilteriUnion_top, top_boxes, BoxIntegral.HasIntegral.tendsto, BoxIntegral.IntegrationParams.eventually_isPartition, isPartitionTop, BoxIntegral.IntegrationParams.hasBasis_toFilteriUnion_top, compl_top, biUnion_top, iUnion_top, distortion_top, splitMany_empty, BoxIntegral.integrable_iff_cauchy, split_of_notMem_Ioo, mem_top
instSemilatticeInf 📖	CompOp	11 math math: iUnion_inf, inf_split, exists_splitMany_inf_eq_filter_of_finite, IsPartition.inf, splitMany_insert, BoxIntegral.integralSum_sub_partitions, mem_inf, inf_def, inf_splitMany, eventually_splitMany_inf_eq_filter, BoxIntegral.TaggedPrepartition.infPrepartition_toPrepartition
ofWithBot 📖	CompOp	6 math math: le_ofWithBot, ofWithBot_le, mem_ofWithBot, iUnion_ofWithBot, ofWithBot_mono, sum_ofWithBot
partialOrder 📖	CompOp	1 math math: monotone_restrict
restrict 📖	CompOp	13 math math: biUnion_le_iff, restrict_biUnion, mem_restrict', restrict_mono, monotone_restrict, restrict_self, iUnion_restrict, inf_def, mem_restrict, le_biUnion_iff, restrict_boxes_of_le, restrict_split, IsPartition.restrict
single 📖	CompOp	7 math math: BoxIntegral.IntegrationParams.tendsto_embedBox_toFilteriUnion_top, BoxIntegral.Integrable.to_subbox_aux, mem_single, single_boxes, BoxIntegral.Integrable.tendsto_integralSum_toFilteriUnion_single, isPartition_single_iff, iUnion_single

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
biUnionIndex_le 📖	mathematical	—	BoxIntegral.Box BoxIntegral.Box.instLE biUnionIndex	—	le_of_mem biUnionIndex_mem biUnionIndex.eq_1 le_refl
biUnionIndex_mem 📖	mathematical	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox biUnion	biUnionIndex	—	biUnionIndex.eq_1 mem_biUnion
biUnionIndex_of_mem 📖	mathematical	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox	biUnionIndex	—	mem_biUnion eq_of_le_of_le biUnionIndex_mem le_biUnionIndex le_of_mem
biUnion_assoc 📖	mathematical	—	biUnion biUnionIndex	—	ext biUnionIndex_of_mem
biUnion_boxes 📖	mathematical	—	boxes biUnion Finset.biUnion BoxIntegral.Box	—	—
biUnion_congr 📖	mathematical	—	biUnion	—	ext
biUnion_congr_of_le 📖	mathematical	—	biUnion	—	biUnion_congr le_of_mem
biUnion_le 📖	mathematical	—	BoxIntegral.Prepartition instLE biUnion	—	mem_biUnion le_of_mem
biUnion_le_iff 📖	mathematical	—	BoxIntegral.Prepartition instLE biUnion restrict	—	restrict_biUnion restrict_mono mem_biUnion mem_restrict LE.le.trans WithBot.coe_le_coe Eq.trans_le inf_le_right
biUnion_top 📖	mathematical	—	biUnion Top.top BoxIntegral.Prepartition OrderTop.toTop instLE instOrderTop	—	ext
bot_boxes 📖	mathematical	—	boxes Bot.bot BoxIntegral.Prepartition OrderBot.toBot instLE instOrderBot Finset BoxIntegral.Box Finset.instEmptyCollection	—	—
card_filter_mem_Icc_le 📖	mathematical	—	Finset.card BoxIntegral.Box Finset.filter Set Set.instMembership DFunLike.coe OrderEmbedding BoxIntegral.Box.instLE Set.instLE instFunLikeOrderEmbedding BoxIntegral.Box.Icc boxes Monoid.toNatPow Nat.instMonoid Fintype.card	—	Fintype.card_set Finset.card_le_card_of_injOn Finset.mem_univ Finset.coe_filter injOn_setOf_mem_Icc_setOf_lower_eq
disjUnion_boxes 📖	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 iUnion	boxes disjUnion Finset BoxIntegral.Box Finset.instUnion	—	—
disjoint_boxes_of_disjoint_iUnion 📖	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 iUnion	Finset BoxIntegral.Box Finset.partialOrder Finset.instOrderBot boxes	—	Finset.disjoint_left Disjoint.le_bot Disjoint.mono subset_iUnion BoxIntegral.Box.upper_mem
disjoint_coe_of_mem 📖	mathematical	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox	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 BoxIntegral.Box.toSet	—	pairwiseDisjoint
distortion_biUnion 📖	mathematical	—	distortion biUnion Finset.sup NNReal BoxIntegral.Box instSemilatticeSupNNReal NNReal.instOrderBot boxes	—	Finset.sup_biUnion
distortion_bot 📖	mathematical	—	distortion Bot.bot BoxIntegral.Prepartition OrderBot.toBot instLE instOrderBot NNReal instZeroNNReal	—	Finset.sup_empty
distortion_disjUnion 📖	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 iUnion	distortion disjUnion NNReal NNReal.instMax	—	Finset.sup_union
distortion_le_iff 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal distortion BoxIntegral.Box.distortion	—	Finset.sup_le_iff
distortion_le_of_mem 📖	mathematical	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal BoxIntegral.Box.distortion distortion	—	Finset.le_sup
distortion_of_const 📖	mathematical	Finset.Nonempty BoxIntegral.Box boxes BoxIntegral.Box.distortion	distortion	—	Finset.sup_congr Finset.sup_const
distortion_top 📖	mathematical	—	distortion Top.top BoxIntegral.Prepartition OrderTop.toTop instLE instOrderTop BoxIntegral.Box.distortion	—	Finset.sup_singleton
eq_of_boxes_subset_iUnion_superset 📖	—	Finset BoxIntegral.Box Finset.instHasSubset boxes Set Set.instHasSubset iUnion	—	—	le_antisymm le_rfl le_iff_nonempty_imp_le_and_iUnion_subset Eq.le eq_of_mem_of_mem
eq_of_le 📖	—	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox BoxIntegral.Box.instLE	—	—	eq_of_le_of_le le_rfl
eq_of_le_of_le 📖	—	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox BoxIntegral.Box.instLE	—	—	eq_of_mem_of_mem BoxIntegral.Box.upper_mem
eq_of_mem_of_mem 📖	—	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox BoxIntegral.Box.instMembershipForallReal	—	—	by_contra Disjoint.le_bot disjoint_coe_of_mem
ext 📖	—	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox	—	—	injective_boxes Finset.ext
ext_iff 📖	mathematical	—	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox	—	ext
filter_boxes 📖	mathematical	—	boxes filter Finset.filter BoxIntegral.Box	—	—
filter_le 📖	mathematical	—	BoxIntegral.Prepartition instLE filter	—	mem_filter le_rfl
filter_of_true 📖	mathematical	—	filter	—	ext
filter_true 📖	mathematical	—	filter	—	filter_of_true
iUnion_biUnion 📖	mathematical	—	iUnion biUnion Set.iUnion BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox	—	Set.iUnion_congr_Prop Set.iUnion_exists Set.biUnion_and'
iUnion_biUnion_partition 📖	mathematical	IsPartition	iUnion biUnion	—	iUnion_biUnion Set.iUnion_congr_of_surjective IsPartition.iUnion_eq
iUnion_bot 📖	mathematical	—	iUnion Bot.bot BoxIntegral.Prepartition OrderBot.toBot instLE instOrderBot Set Set.instEmptyCollection	—	iUnion_eq_empty
iUnion_def 📖	mathematical	—	iUnion Set.iUnion BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox BoxIntegral.Box.toSet	—	—
iUnion_def' 📖	mathematical	—	iUnion Set.iUnion BoxIntegral.Box Finset Finset.instMembership boxes BoxIntegral.Box.toSet	—	—
iUnion_disjUnion 📖	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 iUnion	disjUnion Set.instUnion	—	Set.iUnion_congr_Prop Set.iUnion_or Set.iUnion_union_distrib
iUnion_eq_empty 📖	mathematical	—	iUnion Set Set.instEmptyCollection Bot.bot BoxIntegral.Prepartition OrderBot.toBot instLE instOrderBot	—	injective_boxes
iUnion_filter_not 📖	mathematical	—	iUnion filter Set Set.instSDiff	—	Set.iUnion_congr_Prop Finset.coe_filter Set.biUnion_diff_biUnion_eq Set.PairwiseDisjoint.eq_1 Set.union_eq_left filter_boxes pairwiseDisjoint
iUnion_inf 📖	mathematical	—	iUnion BoxIntegral.Prepartition SemilatticeInf.toMin instSemilatticeInf Set Set.instInter	—	iUnion_biUnion Set.iUnion_congr_Prop iUnion_restrict
iUnion_mono 📖	mathematical	BoxIntegral.Prepartition instLE	Set Set.instHasSubset iUnion	—	mem_iUnion
iUnion_ofWithBot 📖	mathematical	WithBot BoxIntegral.Box Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder BoxIntegral.Box.instPartialOrder WithBot.some Set.Pairwise SetLike.coe Finset Finset.instSetLike Disjoint WithBot.instPartialOrder WithBot.instOrderBot	iUnion ofWithBot Set.iUnion Finset.instMembership BoxIntegral.Box.withBotToSet	—	Set.iUnion_congr_Prop Set.iUnion_comm Set.iUnion_iUnion_eq_right
iUnion_restrict 📖	mathematical	—	iUnion restrict Set Set.instInter BoxIntegral.Box.toSet	—	iUnion_ofWithBot Set.iUnion_congr_Prop Set.iUnion_exists Set.biUnion_and' Set.iUnion_iUnion_eq_right BoxIntegral.Box.coe_inf
iUnion_single 📖	mathematical	BoxIntegral.Box BoxIntegral.Box.instLE	iUnion single BoxIntegral.Box.toSet	—	Set.iUnion_congr_Prop Set.iUnion_iUnion_eq_left
iUnion_subset 📖	mathematical	—	Set Set.instHasSubset iUnion BoxIntegral.Box.toSet	—	Set.iUnion₂_subset le_of_mem'
iUnion_top 📖	mathematical	—	iUnion Top.top BoxIntegral.Prepartition OrderTop.toTop instLE instOrderTop BoxIntegral.Box.toSet	—	Set.iUnion_congr_Prop Set.iUnion_iUnion_eq_left
inf_def 📖	mathematical	—	BoxIntegral.Prepartition SemilatticeInf.toMin instSemilatticeInf biUnion restrict	—	—
injOn_setOf_mem_Icc_setOf_lower_eq 📖	mathematical	—	Set.InjOn BoxIntegral.Box Set setOf Real BoxIntegral.Box.lower BoxIntegral.Prepartition instMembershipBox Set.instMembership DFunLike.coe OrderEmbedding BoxIntegral.Box.instLE Set.instLE instFunLikeOrderEmbedding BoxIntegral.Box.Icc	—	LE.le.eq_or_lt BoxIntegral.Box.lower_lt_upper Set.Ioc_inter_Ioc sup_idem Set.nonempty_Ioc lt_min LE.le.lt_of_ne LT.lt.ne eq_of_mem_of_mem
injective_boxes 📖	mathematical	—	BoxIntegral.Prepartition Finset BoxIntegral.Box boxes	—	—
isPartitionDisjUnionOfEqDiff 📖	mathematical	iUnion Set Set.instSDiff BoxIntegral.Box.toSet	IsPartition disjUnion Disjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice disjoint_sdiff_self_right BooleanAlgebra.toGeneralizedBooleanAlgebra Set.instBooleanAlgebra	—	disjoint_sdiff_self_right isPartition_iff_iUnion_eq iUnion_disjUnion Set.union_diff_self iUnion_subset
isPartitionTop 📖	mathematical	—	IsPartition Top.top BoxIntegral.Prepartition OrderTop.toTop instLE instOrderTop	—	mem_top
isPartition_iff_iUnion_eq 📖	mathematical	—	IsPartition iUnion BoxIntegral.Box.toSet	—	iUnion_subset
isPartition_single_iff 📖	mathematical	BoxIntegral.Box BoxIntegral.Box.instLE	IsPartition single	—	iUnion_single
le_biUnionIndex 📖	mathematical	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox biUnion	BoxIntegral.Box.instLE biUnionIndex	—	le_of_mem mem_biUnionIndex
le_biUnion_iff 📖	mathematical	—	BoxIntegral.Prepartition instLE biUnion restrict	—	LE.le.trans biUnion_le restrict_biUnion restrict_mono mem_restrict inf_of_le_right WithBot.coe_le_coe mem_biUnion
le_def 📖	mathematical	—	BoxIntegral.Prepartition instLE BoxIntegral.Box instMembershipBox BoxIntegral.Box.instLE	—	—
le_iff_nonempty_imp_le_and_iUnion_subset 📖	mathematical	—	BoxIntegral.Prepartition instLE BoxIntegral.Box BoxIntegral.Box.instLE Set Set.instHasSubset iUnion	—	eq_of_mem_of_mem iUnion_mono BoxIntegral.Box.upper_mem
le_ofWithBot 📖	mathematical	WithBot BoxIntegral.Box Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder BoxIntegral.Box.instPartialOrder WithBot.some Set.Pairwise SetLike.coe Finset Finset.instSetLike Disjoint WithBot.instPartialOrder WithBot.instOrderBot Finset.instMembership	BoxIntegral.Prepartition instLE ofWithBot	—	CanLift.prf WithBot.canLift ne_bot_of_le_ne_bot WithBot.coe_ne_bot mem_ofWithBot WithBot.coe_le_coe
le_of_mem 📖	mathematical	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox	BoxIntegral.Box.instLE	—	le_of_mem'
le_of_mem' 📖	mathematical	BoxIntegral.Box Finset Finset.instMembership boxes	BoxIntegral.Box.instLE	—	—
lower_le_lower 📖	mathematical	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox	Pi.hasLe Real Real.instLE BoxIntegral.Box.lower	—	BoxIntegral.Box.antitone_lower le_of_mem
mem_biUnion 📖	mathematical	—	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox biUnion	—	—
mem_biUnionIndex 📖	mathematical	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox biUnion	biUnionIndex	—	mem_biUnion
mem_boxes 📖	mathematical	—	BoxIntegral.Box Finset Finset.instMembership boxes BoxIntegral.Prepartition instMembershipBox	—	—
mem_disjUnion 📖	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 iUnion	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox disjUnion	—	Finset.mem_union
mem_filter 📖	mathematical	—	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox filter	—	Finset.mem_filter
mem_iUnion 📖	mathematical	—	Set Set.instMembership iUnion BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox BoxIntegral.Box.instMembershipForallReal	—	BoxIntegral.Box.mem_coe Set.mem_iUnion₂
mem_inf 📖	mathematical	—	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox SemilatticeInf.toMin instSemilatticeInf WithBot.some WithBot BoxIntegral.Box.WithBot.inf	—	—
mem_mk 📖	mathematical	BoxIntegral.Box BoxIntegral.Box.instLE Set.Pairwise SetLike.coe Finset Finset.instSetLike Function.onFun Set Disjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice BoxIntegral.Box.toSet	BoxIntegral.Prepartition instMembershipBox Finset.instMembership	—	—
mem_ofWithBot 📖	mathematical	WithBot BoxIntegral.Box Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder BoxIntegral.Box.instPartialOrder WithBot.some Set.Pairwise SetLike.coe Finset Finset.instSetLike Disjoint WithBot.instPartialOrder WithBot.instOrderBot	BoxIntegral.Prepartition instMembershipBox ofWithBot Finset.instMembership	—	Finset.mem_eraseNone
mem_restrict 📖	mathematical	—	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox restrict WithBot.some WithBot BoxIntegral.Box.WithBot.inf	—	—
mem_restrict' 📖	mathematical	—	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox restrict BoxIntegral.Box.toSet Set Set.instInter	—	BoxIntegral.Box.coe_inf
mem_single 📖	mathematical	BoxIntegral.Box BoxIntegral.Box.instLE	BoxIntegral.Prepartition instMembershipBox single	—	Finset.mem_singleton
mem_top 📖	mathematical	—	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox Top.top OrderTop.toTop instLE instOrderTop	—	Finset.mem_singleton
monotone_restrict 📖	mathematical	—	Monotone BoxIntegral.Prepartition PartialOrder.toPreorder partialOrder restrict	—	restrict_mono
notMem_bot 📖	mathematical	—	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox Bot.bot OrderBot.toBot instLE instOrderBot	—	Finset.notMem_empty
ofWithBot_le 📖	mathematical	WithBot BoxIntegral.Box Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder BoxIntegral.Box.instPartialOrder WithBot.some Set.Pairwise SetLike.coe Finset Finset.instSetLike Disjoint WithBot.instPartialOrder WithBot.instOrderBot BoxIntegral.Prepartition instMembershipBox	instLE ofWithBot	—	WithBot.coe_ne_bot
ofWithBot_mono 📖	mathematical	WithBot BoxIntegral.Box Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder BoxIntegral.Box.instPartialOrder WithBot.some Set.Pairwise SetLike.coe Finset Finset.instSetLike Disjoint WithBot.instPartialOrder WithBot.instOrderBot Finset.instMembership	BoxIntegral.Prepartition instLE ofWithBot	—	le_ofWithBot mem_ofWithBot WithBot.coe_ne_bot
pairwiseDisjoint 📖	mathematical	—	Set.Pairwise BoxIntegral.Box SetLike.coe Finset Finset.instSetLike boxes Function.onFun Set Disjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice BoxIntegral.Box.toSet	—	—
restrict_biUnion 📖	mathematical	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox	restrict biUnion	—	eq_of_boxes_subset_iUnion_superset mem_restrict mem_biUnion inf_of_le_right WithBot.coe_le_coe le_of_mem iUnion_restrict iUnion_biUnion eq_of_mem_of_mem iUnion_subset
restrict_boxes_of_le 📖	mathematical	BoxIntegral.Box BoxIntegral.Box.instLE	boxes restrict	—	Finset.eraseNone_eq_biUnion Finset.image_biUnion Finset.biUnion_congr inf_of_le_right WithBot.coe_le_coe LE.le.trans le_of_mem WithBot.some_eq_coe Option.toFinset_some Finset.biUnion_singleton_eq_self
restrict_mono 📖	mathematical	BoxIntegral.Prepartition instLE	restrict	—	ofWithBot_mono Finset.mem_image Finset.mem_image_of_mem inf_le_inf_left WithBot.coe_le_coe
restrict_self 📖	mathematical	—	restrict	—	injective_boxes restrict_boxes_of_le le_rfl
single_boxes 📖	mathematical	BoxIntegral.Box BoxIntegral.Box.instLE	boxes single Finset Finset.instSingleton	—	—
subset_iUnion 📖	mathematical	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox	Set Set.instHasSubset BoxIntegral.Box.toSet iUnion	—	Set.subset_biUnion_of_mem
sum_biUnion_boxes 📖	mathematical	—	Finset.sum BoxIntegral.Box Finset.biUnion boxes	—	Finset.sum_biUnion Finset.disjoint_left eq_of_le_of_le le_of_mem
sum_disj_union_boxes 📖	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 iUnion	Finset.sum BoxIntegral.Box Finset Finset.instUnion boxes AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	Finset.sum_union disjoint_boxes_of_disjoint_iUnion
sum_fiberwise 📖	mathematical	—	Finset.sum Finset.image BoxIntegral.Box boxes filter	—	Finset.sum_congr Finset.sum_fiberwise_of_maps_to Finset.mem_image_of_mem
sum_ofWithBot 📖	mathematical	WithBot BoxIntegral.Box Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder BoxIntegral.Box.instPartialOrder WithBot.some Set.Pairwise SetLike.coe Finset Finset.instSetLike Disjoint WithBot.instPartialOrder WithBot.instOrderBot	Finset.sum boxes ofWithBot Option.elim' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Finset.sum_eraseNone
top_boxes 📖	mathematical	—	boxes Top.top BoxIntegral.Prepartition OrderTop.toTop instLE instOrderTop BoxIntegral.Box Finset Finset.instSingleton	—	—
upper_le_upper 📖	mathematical	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox	Pi.hasLe Real Real.instLE BoxIntegral.Box.upper	—	BoxIntegral.Box.monotone_upper le_of_mem

BoxIntegral.Prepartition.IsPartition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
biUnion 📖	mathematical	BoxIntegral.Prepartition.IsPartition	BoxIntegral.Prepartition.biUnion	—	BoxIntegral.Prepartition.mem_biUnion
eq_of_boxes_subset 📖	—	BoxIntegral.Prepartition.IsPartition Finset BoxIntegral.Box Finset.instHasSubset BoxIntegral.Prepartition.boxes	—	—	BoxIntegral.Prepartition.eq_of_boxes_subset_iUnion_superset iUnion_subset
existsUnique 📖	mathematical	BoxIntegral.Prepartition.IsPartition BoxIntegral.Box BoxIntegral.Box.instMembershipForallReal	ExistsUnique BoxIntegral.Prepartition BoxIntegral.Prepartition.instMembershipBox	—	ExistsUnique.intro BoxIntegral.Prepartition.eq_of_mem_of_mem
iUnion_eq 📖	mathematical	BoxIntegral.Prepartition.IsPartition	BoxIntegral.Prepartition.iUnion BoxIntegral.Box.toSet	—	BoxIntegral.Prepartition.isPartition_iff_iUnion_eq
iUnion_subset 📖	mathematical	BoxIntegral.Prepartition.IsPartition	Set Set.instHasSubset BoxIntegral.Prepartition.iUnion	—	BoxIntegral.Prepartition.iUnion_subset iUnion_eq
inf 📖	mathematical	BoxIntegral.Prepartition.IsPartition	BoxIntegral.Prepartition SemilatticeInf.toMin BoxIntegral.Prepartition.instSemilatticeInf	—	BoxIntegral.Prepartition.isPartition_iff_iUnion_eq BoxIntegral.Prepartition.iUnion_inf iUnion_eq Set.inter_self
le_iff 📖	mathematical	BoxIntegral.Prepartition.IsPartition	BoxIntegral.Prepartition BoxIntegral.Prepartition.instLE BoxIntegral.Box BoxIntegral.Box.instLE	—	BoxIntegral.Prepartition.le_iff_nonempty_imp_le_and_iUnion_subset iUnion_subset
nonempty_boxes 📖	mathematical	BoxIntegral.Prepartition.IsPartition	Finset.Nonempty BoxIntegral.Box BoxIntegral.Prepartition.boxes	—	BoxIntegral.Box.upper_mem
restrict 📖	mathematical	BoxIntegral.Prepartition.IsPartition BoxIntegral.Box BoxIntegral.Box.instLE	BoxIntegral.Prepartition.restrict	—	BoxIntegral.Prepartition.isPartition_iff_iUnion_eq BoxIntegral.Prepartition.iUnion_restrict iUnion_eq

---

← Back to Index