Commit 2023-04-26 04:18 f4c36e31

View on Github →

feat: port Analysis.BoxIntegral.Partition.Basic (#3438)

Estimated changes

Modified Mathlib.lean

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

added theorem BoxIntegral.Prepartition.IsPartition.eq_of_boxes_subset

added theorem BoxIntegral.Prepartition.IsPartition.le_iff

added theorem BoxIntegral.Prepartition.IsPartition.nonempty_boxes

added theorem BoxIntegral.Prepartition.IsPartition.unionᵢ_eq

added theorem BoxIntegral.Prepartition.IsPartition.unionᵢ_subset

added def BoxIntegral.Prepartition.IsPartition

added theorem BoxIntegral.Prepartition.bot_boxes

added def BoxIntegral.Prepartition.bunionᵢ

added def BoxIntegral.Prepartition.bunionᵢIndex

added theorem BoxIntegral.Prepartition.bunionᵢIndex_le

added theorem BoxIntegral.Prepartition.bunionᵢIndex_mem

added theorem BoxIntegral.Prepartition.bunionᵢIndex_of_mem

added theorem BoxIntegral.Prepartition.bunionᵢ_assoc

added theorem BoxIntegral.Prepartition.bunionᵢ_congr

added theorem BoxIntegral.Prepartition.bunionᵢ_congr_of_le

added theorem BoxIntegral.Prepartition.bunionᵢ_le

added theorem BoxIntegral.Prepartition.bunionᵢ_le_iff

added theorem BoxIntegral.Prepartition.bunionᵢ_top

added theorem BoxIntegral.Prepartition.card_filter_mem_Icc_le

added def BoxIntegral.Prepartition.disjUnion

added theorem BoxIntegral.Prepartition.disjoint_boxes_of_disjoint_unionᵢ

added theorem BoxIntegral.Prepartition.disjoint_coe_of_mem

added def BoxIntegral.Prepartition.distortion

added theorem BoxIntegral.Prepartition.distortion_bot

added theorem BoxIntegral.Prepartition.distortion_bunionᵢ

added theorem BoxIntegral.Prepartition.distortion_disjUnion

added theorem BoxIntegral.Prepartition.distortion_le_iff

added theorem BoxIntegral.Prepartition.distortion_le_of_mem

added theorem BoxIntegral.Prepartition.distortion_of_const

added theorem BoxIntegral.Prepartition.distortion_top

added theorem BoxIntegral.Prepartition.eq_of_boxes_subset_unionᵢ_superset

added theorem BoxIntegral.Prepartition.eq_of_le

added theorem BoxIntegral.Prepartition.eq_of_le_of_le

added theorem BoxIntegral.Prepartition.eq_of_mem_of_mem

added theorem BoxIntegral.Prepartition.ext

added def BoxIntegral.Prepartition.filter

added theorem BoxIntegral.Prepartition.filter_le

added theorem BoxIntegral.Prepartition.filter_of_true

added theorem BoxIntegral.Prepartition.filter_true

added theorem BoxIntegral.Prepartition.inf_def

added theorem BoxIntegral.Prepartition.injOn_setOf_mem_Icc_setOf_lower_eq

added theorem BoxIntegral.Prepartition.injective_boxes

added theorem BoxIntegral.Prepartition.isPartitionDisjUnionOfEqDiff

added theorem BoxIntegral.Prepartition.isPartitionTop

added theorem BoxIntegral.Prepartition.isPartition_iff_unionᵢ_eq

added theorem BoxIntegral.Prepartition.isPartition_single_iff

added theorem BoxIntegral.Prepartition.le_bunionᵢIndex

added theorem BoxIntegral.Prepartition.le_bunionᵢ_iff

added theorem BoxIntegral.Prepartition.le_def

added theorem BoxIntegral.Prepartition.le_iff_nonempty_imp_le_and_unionᵢ_subset

added theorem BoxIntegral.Prepartition.le_ofWithBot

added theorem BoxIntegral.Prepartition.le_of_mem

added theorem BoxIntegral.Prepartition.lower_le_lower

added theorem BoxIntegral.Prepartition.mem_boxes

added theorem BoxIntegral.Prepartition.mem_bunionᵢ

added theorem BoxIntegral.Prepartition.mem_bunionᵢIndex

added theorem BoxIntegral.Prepartition.mem_disjUnion

added theorem BoxIntegral.Prepartition.mem_filter

added theorem BoxIntegral.Prepartition.mem_inf

added theorem BoxIntegral.Prepartition.mem_mk

added theorem BoxIntegral.Prepartition.mem_ofWithBot

added theorem BoxIntegral.Prepartition.mem_restrict'

added theorem BoxIntegral.Prepartition.mem_restrict

added theorem BoxIntegral.Prepartition.mem_single

added theorem BoxIntegral.Prepartition.mem_top

added theorem BoxIntegral.Prepartition.mem_unionᵢ

added theorem BoxIntegral.Prepartition.monotone_restrict

added theorem BoxIntegral.Prepartition.not_mem_bot

added def BoxIntegral.Prepartition.ofWithBot

added theorem BoxIntegral.Prepartition.ofWithBot_le

added theorem BoxIntegral.Prepartition.ofWithBot_mono

added def BoxIntegral.Prepartition.restrict

added theorem BoxIntegral.Prepartition.restrict_boxes_of_le

added theorem BoxIntegral.Prepartition.restrict_bunionᵢ

added theorem BoxIntegral.Prepartition.restrict_mono

added theorem BoxIntegral.Prepartition.restrict_self

added def BoxIntegral.Prepartition.single

added theorem BoxIntegral.Prepartition.subset_unionᵢ

added theorem BoxIntegral.Prepartition.sum_bunionᵢ_boxes

added theorem BoxIntegral.Prepartition.sum_disj_union_boxes

added theorem BoxIntegral.Prepartition.sum_fiberwise

added theorem BoxIntegral.Prepartition.sum_ofWithBot

added theorem BoxIntegral.Prepartition.top_boxes

added theorem BoxIntegral.Prepartition.unionᵢ_bot

added theorem BoxIntegral.Prepartition.unionᵢ_bunionᵢ

added theorem BoxIntegral.Prepartition.unionᵢ_bunionᵢ_partition

added theorem BoxIntegral.Prepartition.unionᵢ_def'

added theorem BoxIntegral.Prepartition.unionᵢ_def

added theorem BoxIntegral.Prepartition.unionᵢ_disjUnion

added theorem BoxIntegral.Prepartition.unionᵢ_eq_empty

added theorem BoxIntegral.Prepartition.unionᵢ_filter_not

added theorem BoxIntegral.Prepartition.unionᵢ_inf

added theorem BoxIntegral.Prepartition.unionᵢ_mono

added theorem BoxIntegral.Prepartition.unionᵢ_ofWithBot

added theorem BoxIntegral.Prepartition.unionᵢ_restrict

added theorem BoxIntegral.Prepartition.unionᵢ_single

added theorem BoxIntegral.Prepartition.unionᵢ_subset

added theorem BoxIntegral.Prepartition.unionᵢ_top

added theorem BoxIntegral.Prepartition.upper_le_upper

added structure BoxIntegral.Prepartition