Commit 2023-04-17 10:44 24004588

View on Github →

feat: port Analysis.BoxIntegral.Box.SubboxInduction (#3440)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/BoxIntegral/Box/SubboxInduction.lean

added theorem BoxIntegral.Box.disjoint_splitCenterBox

added theorem BoxIntegral.Box.exists_mem_splitCenterBox

added theorem BoxIntegral.Box.injective_splitCenterBox

added theorem BoxIntegral.Box.mem_splitCenterBox

added def BoxIntegral.Box.splitCenterBox

added def BoxIntegral.Box.splitCenterBoxEmb

added theorem BoxIntegral.Box.splitCenterBox_le

added theorem BoxIntegral.Box.subbox_induction_on'

added theorem BoxIntegral.Box.unionᵢ_coe_splitCenterBox

added theorem BoxIntegral.Box.upper_sub_lower_splitCenterBox