Commit 2023-04-26 11:37 6aa4d442

View on Github →

feat: port Analysis.BoxIntegral.Partition.Split (#3658)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/BoxIntegral/Partition/Split.lean

added theorem BoxIntegral.Box.coe_splitLower

added theorem BoxIntegral.Box.coe_splitUpper

added theorem BoxIntegral.Box.disjoint_splitLower_splitUpper

added def BoxIntegral.Box.splitLower

added theorem BoxIntegral.Box.splitLower_def

added theorem BoxIntegral.Box.splitLower_eq_bot

added theorem BoxIntegral.Box.splitLower_eq_self

added theorem BoxIntegral.Box.splitLower_le

added theorem BoxIntegral.Box.splitLower_ne_splitUpper

added def BoxIntegral.Box.splitUpper

added theorem BoxIntegral.Box.splitUpper_def

added theorem BoxIntegral.Box.splitUpper_eq_bot

added theorem BoxIntegral.Box.splitUpper_eq_self

added theorem BoxIntegral.Box.splitUpper_le

added theorem BoxIntegral.Prepartition.IsPartition.compl_eq_bot

added theorem BoxIntegral.Prepartition.IsPartition.exists_splitMany_le

added theorem BoxIntegral.Prepartition.coe_eq_of_mem_split_of_lt_mem

added theorem BoxIntegral.Prepartition.coe_eq_of_mem_split_of_mem_le

added def BoxIntegral.Prepartition.compl

added theorem BoxIntegral.Prepartition.compl_congr

added theorem BoxIntegral.Prepartition.compl_top

added theorem BoxIntegral.Prepartition.eventually_not_disjoint_imp_le_of_mem_splitMany

added theorem BoxIntegral.Prepartition.eventually_splitMany_inf_eq_filter

added theorem BoxIntegral.Prepartition.exists_splitMany_inf_eq_filter_of_finite

added theorem BoxIntegral.Prepartition.exists_unionᵢ_eq_diff

added theorem BoxIntegral.Prepartition.inf_split

added theorem BoxIntegral.Prepartition.inf_splitMany

added theorem BoxIntegral.Prepartition.isPartitionSplit

added theorem BoxIntegral.Prepartition.isPartition_splitMany

added theorem BoxIntegral.Prepartition.mem_split_iff'

added theorem BoxIntegral.Prepartition.mem_split_iff

added theorem BoxIntegral.Prepartition.not_disjoint_imp_le_of_subset_of_mem_splitMany

added theorem BoxIntegral.Prepartition.restrict_split

added def BoxIntegral.Prepartition.split

added def BoxIntegral.Prepartition.splitMany

added theorem BoxIntegral.Prepartition.splitMany_empty

added theorem BoxIntegral.Prepartition.splitMany_insert

added theorem BoxIntegral.Prepartition.splitMany_le_split

added theorem BoxIntegral.Prepartition.split_of_not_mem_Ioo

added theorem BoxIntegral.Prepartition.sum_split_boxes

added theorem BoxIntegral.Prepartition.unionᵢ_compl

added theorem BoxIntegral.Prepartition.unionᵢ_split

added theorem BoxIntegral.Prepartition.unionᵢ_splitMany