Split

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

Statistics

Metric	Count
Definitions `splitLower`, `splitUpper`, `compl`, `split`, `splitMany`	5
Theorems `coe_splitLower`, `coe_splitUpper`, `disjoint_splitLower_splitUpper`, `splitLower_def`, `splitLower_eq_bot`, `splitLower_eq_self`, `splitLower_le`, `splitLower_ne_splitUpper`, `splitUpper_def`, `splitUpper_eq_bot`, `splitUpper_eq_self`, `splitUpper_le`, `compl_eq_bot`, `exists_splitMany_le`, `coe_eq_of_mem_split_of_lt_mem`, `coe_eq_of_mem_split_of_mem_le`, `compl_congr`, `compl_top`, `eventually_not_disjoint_imp_le_of_mem_splitMany`, `eventually_splitMany_inf_eq_filter`, `exists_iUnion_eq_diff`, `exists_splitMany_inf_eq_filter_of_finite`, `iUnion_compl`, `iUnion_split`, `iUnion_splitMany`, `inf_split`, `inf_splitMany`, `isPartitionSplit`, `isPartition_splitMany`, `mem_split_iff`, `mem_split_iff'`, `not_disjoint_imp_le_of_subset_of_mem_splitMany`, `restrict_split`, `splitMany_empty`, `splitMany_insert`, `splitMany_le_split`, `split_of_notMem_Ioo`, `sum_split_boxes`	38
Total	43

BoxIntegral.Box

Definitions

Name	Category	Theorems
`splitLower` 📖	CompOp	9 math math: `BoxIntegral.BoxAdditiveMap.map_split_add`, `splitLower_def`, `BoxIntegral.Prepartition.mem_split_iff`, `splitLower_le`, `splitLower_eq_bot`, `coe_splitLower`, `disjoint_splitLower_splitUpper`, `splitLower_eq_self`, `BoxIntegral.Prepartition.sum_split_boxes`
`splitUpper` 📖	CompOp	9 math math: `BoxIntegral.BoxAdditiveMap.map_split_add`, `splitUpper_eq_bot`, `BoxIntegral.Prepartition.mem_split_iff`, `splitUpper_le`, `splitUpper_def`, `splitUpper_eq_self`, `disjoint_splitLower_splitUpper`, `BoxIntegral.Prepartition.sum_split_boxes`, `coe_splitUpper`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_splitLower` 📖	mathematical	—	`withBotToSet` `splitLower` `Set` `Set.instInter` `toSet` `setOf` `Real` `Real.instLE`	—	`splitLower.eq_1` `coe_mk'` `Set.ext` `and_forall_ne`
`coe_splitUpper` 📖	mathematical	—	`withBotToSet` `splitUpper` `Set` `Set.instInter` `toSet` `setOf` `Real` `Real.instLT`	—	`splitUpper.eq_1` `coe_mk'` `Set.ext` `Function.forall_update_iff` `and_forall_ne`
`disjoint_splitLower_splitUpper` 📖	mathematical	—	`Disjoint` `WithBot` `BoxIntegral.Box` `WithBot.instPartialOrder` `instPartialOrder` `WithBot.instOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `splitLower` `splitUpper`	—	`disjoint_withBotCoe` `coe_splitLower` `coe_splitUpper` `Disjoint.inf_right'` `Disjoint.inf_left'` `Set.disjoint_left` `not_lt_of_ge`
`splitLower_def` 📖	mathematical	`Real` `Set` `Set.instMembership` `Set.Ioo` `Real.instPreorder` `lower` `upper` `Real.instLT` `Function.forall_update_iff` `Preorder.toLT` `lower_lt_upper`	`splitLower` `WithBot.some` `BoxIntegral.Box` `Function.update`	—	`min_eq_left` `LT.lt.le`
`splitLower_eq_bot` 📖	mathematical	—	`splitLower` `Bot.bot` `WithBot` `BoxIntegral.Box` `WithBot.bot` `Real` `Real.instLE` `lower`	—	`splitLower.eq_1` `mk'_eq_bot` `Function.exists_update_iff` `LT.lt.not_ge` `lower_lt_upper`
`splitLower_eq_self` 📖	mathematical	—	`splitLower` `WithBot.some` `BoxIntegral.Box` `Real` `Real.instLE` `upper`	—	—
`splitLower_le` 📖	mathematical	—	`WithBot` `BoxIntegral.Box` `Preorder.toLE` `WithBot.instPreorder` `PartialOrder.toPreorder` `instPartialOrder` `splitLower` `WithBot.some`	—	`withBotCoe_subset_iff` `coe_splitLower`
`splitLower_ne_splitUpper` 📖	—	—	—	—	`le_or_gt` `splitUpper_eq_self` `splitLower_eq_bot` `WithBot.bot_ne_coe` `Disjoint.ne` `not_le` `disjoint_splitLower_splitUpper`
`splitUpper_def` 📖	mathematical	`Real` `Set` `Set.instMembership` `Set.Ioo` `Real.instPreorder` `lower` `upper` `Real.instLT` `Function.forall_update_iff` `Preorder.toLT` `lower_lt_upper`	`splitUpper` `WithBot.some` `BoxIntegral.Box` `Function.update`	—	`max_eq_left` `LT.lt.le`
`splitUpper_eq_bot` 📖	mathematical	—	`splitUpper` `Bot.bot` `WithBot` `BoxIntegral.Box` `WithBot.bot` `Real` `Real.instLE` `upper`	—	`splitUpper.eq_1` `mk'_eq_bot` `Function.exists_update_iff` `LT.lt.not_ge` `lower_lt_upper`
`splitUpper_eq_self` 📖	mathematical	—	`splitUpper` `WithBot.some` `BoxIntegral.Box` `Real` `Real.instLE` `lower`	—	—
`splitUpper_le` 📖	mathematical	—	`WithBot` `BoxIntegral.Box` `Preorder.toLE` `WithBot.instPreorder` `PartialOrder.toPreorder` `instPartialOrder` `splitUpper` `WithBot.some`	—	`withBotCoe_subset_iff` `coe_splitUpper`

BoxIntegral.Prepartition

Definitions

Name	Category	Theorems
`compl` 📖	CompOp	5 math math: `BoxIntegral.IntegrationParams.toFilterDistortioniUnion_neBot'`, `compl_congr`, `IsPartition.compl_eq_bot`, `compl_top`, `iUnion_compl`
`split` 📖	CompOp	10 math math: `mem_split_iff`, `mem_split_iff'`, `inf_split`, `splitMany_insert`, `splitMany_le_split`, `split_of_notMem_Ioo`, `sum_split_boxes`, `restrict_split`, `isPartitionSplit`, `iUnion_split`
`splitMany` 📖	CompOp	9 math math: `exists_splitMany_inf_eq_filter_of_finite`, `splitMany_empty`, `splitMany_insert`, `splitMany_le_split`, `iUnion_splitMany`, `inf_splitMany`, `IsPartition.exists_splitMany_le`, `eventually_splitMany_inf_eq_filter`, `isPartition_splitMany`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_eq_of_mem_split_of_lt_mem` 📖	mathematical	`BoxIntegral.Box` `BoxIntegral.Prepartition` `instMembershipBox` `split` `BoxIntegral.Box.instMembershipForallReal` `Real` `Real.instLT`	`BoxIntegral.Box.toSet` `Set` `Set.instInter` `setOf`	—	`mem_split_iff'` `LT.lt.not_ge` `BoxIntegral.Box.mem_coe`
`coe_eq_of_mem_split_of_mem_le` 📖	mathematical	`BoxIntegral.Box` `BoxIntegral.Prepartition` `instMembershipBox` `split` `BoxIntegral.Box.instMembershipForallReal` `Real` `Real.instLE`	`BoxIntegral.Box.toSet` `Set` `Set.instInter` `setOf`	—	`mem_split_iff'` `LE.le.not_gt` `BoxIntegral.Box.mem_coe`
`compl_congr` 📖	mathematical	`iUnion`	`compl`	—	`exists_iUnion_eq_diff`
`compl_top` 📖	mathematical	—	`compl` `Top.top` `BoxIntegral.Prepartition` `OrderTop.toTop` `instLE` `instOrderTop` `Bot.bot` `OrderBot.toBot` `instOrderBot`	—	`IsPartition.compl_eq_bot` `isPartitionTop`
`eventually_not_disjoint_imp_le_of_mem_splitMany` 📖	mathematical	—	`Filter.Eventually` `Finset` `Real` `Filter.atTop` `PartialOrder.toPreorder` `Finset.partialOrder`	—	`nonempty_fintype` `Filter.eventually_atTop` `Finset.isDirected_le` `not_disjoint_imp_le_of_subset_of_mem_splitMany` `Finset.mem_biUnion` `Finset.mem_univ`
`eventually_splitMany_inf_eq_filter` 📖	mathematical	—	`Filter.Eventually` `Finset` `Real` `BoxIntegral.Prepartition` `SemilatticeInf.toMin` `instSemilatticeInf` `splitMany` `filter` `Set` `Set.instHasSubset` `BoxIntegral.Box.toSet` `iUnion` `Filter.atTop` `PartialOrder.toPreorder` `Finset.partialOrder`	—	`Filter.Eventually.mono` `eventually_not_disjoint_imp_le_of_mem_splitMany` `le_antisymm` `biUnion_le_iff` `ofWithBot_mono` `Set.Subset.trans` `disjoint_iff` `subset_iUnion` `le_rfl` `le_inf` `Set.mem_iUnion₂` `mem_filter` `BoxIntegral.Box.upper_mem` `BoxIntegral.Box.not_disjoint_coe_iff_nonempty_inter` `filter_le`
`exists_iUnion_eq_diff` 📖	mathematical	—	`iUnion` `Set` `Set.instSDiff` `BoxIntegral.Box.toSet`	—	`Filter.Eventually.exists` `Filter.atTop_neBot` `Finset.isDirected_le` `eventually_splitMany_inf_eq_filter` `iUnion_filter_not` `iUnion_splitMany` `iUnion_inf` `Set.diff_inter_self_eq_diff`
`exists_splitMany_inf_eq_filter_of_finite` 📖	mathematical	—	`BoxIntegral.Prepartition` `SemilatticeInf.toMin` `instSemilatticeInf` `splitMany` `filter` `Set` `Set.instHasSubset` `BoxIntegral.Box.toSet` `iUnion`	—	`Filter.Eventually.exists` `Filter.atTop_neBot` `Finset.isDirected_le` `Set.Finite.eventually_all` `eventually_splitMany_inf_eq_filter`
`iUnion_compl` 📖	mathematical	—	`iUnion` `compl` `Set` `Set.instSDiff` `BoxIntegral.Box.toSet`	—	`exists_iUnion_eq_diff`
`iUnion_split` 📖	mathematical	—	`iUnion` `split` `BoxIntegral.Box.toSet`	—	`iUnion_ofWithBot` `Set.iUnion_congr_Prop` `Set.iUnion_iUnion_eq_or_left` `BoxIntegral.Box.coe_splitLower` `Set.iUnion_iUnion_eq_left` `BoxIntegral.Box.coe_splitUpper` `Set.inter_univ`
`iUnion_splitMany` 📖	mathematical	—	`iUnion` `splitMany` `BoxIntegral.Box.toSet`	—	`IsPartition.iUnion_eq` `isPartition_splitMany`
`inf_split` 📖	mathematical	—	`BoxIntegral.Prepartition` `SemilatticeInf.toMin` `instSemilatticeInf` `split` `biUnion`	—	`biUnion_congr_of_le` `restrict_split`
`inf_splitMany` 📖	mathematical	—	`BoxIntegral.Prepartition` `SemilatticeInf.toMin` `instSemilatticeInf` `splitMany` `biUnion`	—	`Finset.induction_on` `inf_of_le_left` `biUnion_congr` `biUnion_top` `splitMany_insert` `inf_split` `biUnion_assoc`
`isPartitionSplit` 📖	mathematical	—	`IsPartition` `split`	—	`isPartition_iff_iUnion_eq` `iUnion_split`
`isPartition_splitMany` 📖	mathematical	—	`IsPartition` `splitMany`	—	`Finset.induction_on` `splitMany_insert` `inf_split` `IsPartition.biUnion` `isPartitionSplit`
`mem_split_iff` 📖	mathematical	—	`BoxIntegral.Box` `BoxIntegral.Prepartition` `instMembershipBox` `split` `WithBot.some` `BoxIntegral.Box.splitLower` `BoxIntegral.Box.splitUpper`	—	—
`mem_split_iff'` 📖	mathematical	—	`BoxIntegral.Box` `BoxIntegral.Prepartition` `instMembershipBox` `split` `BoxIntegral.Box.toSet` `Set` `Set.instInter` `setOf` `Real` `Real.instLE` `Real.instLT`	—	`BoxIntegral.Box.coe_splitLower` `BoxIntegral.Box.coe_splitUpper`
`not_disjoint_imp_le_of_subset_of_mem_splitMany` 📖	mathematical	`Finset` `Real` `Finset.instHasSubset` `Finset.instInsert` `Real.decidableEq` `BoxIntegral.Box.lower` `Finset.instSingleton` `BoxIntegral.Box.upper` `BoxIntegral.Box` `BoxIntegral.Prepartition` `instMembershipBox` `splitMany` `Disjoint` `WithBot` `WithBot.instPartialOrder` `BoxIntegral.Box.instPartialOrder` `WithBot.instOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `WithBot.some`	`BoxIntegral.Box.instLE`	—	`BoxIntegral.Box.not_disjoint_coe_iff_nonempty_inter` `splitMany_le_split` `coe_eq_of_mem_split_of_lt_mem` `BoxIntegral.Box.coe_subset_coe` `coe_eq_of_mem_split_of_mem_le`
`restrict_split` 📖	mathematical	`BoxIntegral.Box` `BoxIntegral.Box.instLE`	`restrict` `split`	—	`IsPartition.eq_of_boxes_subset` `IsPartition.restrict` `isPartitionSplit` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.inter_subset_left` `Set.inter_left_comm`
`splitMany_empty` 📖	mathematical	—	`splitMany` `Finset` `Real` `Finset.instEmptyCollection` `Top.top` `BoxIntegral.Prepartition` `OrderTop.toTop` `instLE` `instOrderTop`	—	—
`splitMany_insert` 📖	mathematical	—	`splitMany` `Real` `Finset` `Finset.instInsert` `Real.decidableEq` `BoxIntegral.Prepartition` `SemilatticeInf.toMin` `instSemilatticeInf` `split`	—	`splitMany.eq_1` `Finset.inf_insert` `inf_comm`
`splitMany_le_split` 📖	mathematical	`Real` `Finset` `Finset.instMembership`	`BoxIntegral.Prepartition` `instLE` `splitMany` `split`	—	`Finset.inf_le`
`split_of_notMem_Ioo` 📖	mathematical	`Real` `Set` `Set.instMembership` `Set.Ioo` `Real.instPreorder` `BoxIntegral.Box.lower` `BoxIntegral.Box.upper`	`split` `Top.top` `BoxIntegral.Prepartition` `OrderTop.toTop` `instLE` `instOrderTop`	—	`IsPartition.eq_of_boxes_subset` `isPartitionTop` `mem_boxes` `mem_split_iff` `not_lt` `not_and_or` `Set.mem_Ioo` `BoxIntegral.Box.splitUpper_eq_self` `BoxIntegral.Box.splitLower_eq_self` `mem_top`
`sum_split_boxes` 📖	mathematical	—	`Finset.sum` `BoxIntegral.Box` `boxes` `split` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Option.elim'` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `BoxIntegral.Box.splitLower` `BoxIntegral.Box.splitUpper`	—	`split.eq_1` `sum_ofWithBot` `Finset.sum_pair` `BoxIntegral.Box.splitLower_ne_splitUpper`

BoxIntegral.Prepartition.IsPartition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compl_eq_bot` 📖	mathematical	`BoxIntegral.Prepartition.IsPartition`	`BoxIntegral.Prepartition.compl` `Bot.bot` `BoxIntegral.Prepartition` `OrderBot.toBot` `BoxIntegral.Prepartition.instLE` `BoxIntegral.Prepartition.instOrderBot`	—	`BoxIntegral.Prepartition.iUnion_eq_empty` `BoxIntegral.Prepartition.iUnion_compl` `iUnion_eq` `Set.diff_self`
`exists_splitMany_le` 📖	mathematical	`BoxIntegral.Prepartition.IsPartition`	`BoxIntegral.Prepartition` `BoxIntegral.Prepartition.instLE` `BoxIntegral.Prepartition.splitMany`	—	`inf_eq_right` `BoxIntegral.Prepartition.filter_of_true` `BoxIntegral.Prepartition.le_of_mem` `iUnion_eq` `Filter.Eventually.exists` `Filter.atTop_neBot` `Finset.isDirected_le` `BoxIntegral.Prepartition.eventually_splitMany_inf_eq_filter`

---

← Back to Index