Commit 2023-04-14 15:26 0d49462a

View on Github →

feat: port Analysis.BoxIntegral.Box.Basic (#2625)

Estimated changes

Modified Mathlib.lean

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

added theorem BoxIntegral.Box.antitone_lower

added theorem BoxIntegral.Box.bUnion_coe_eq_coe

added theorem BoxIntegral.Box.coe_bot

added theorem BoxIntegral.Box.coe_coe

added theorem BoxIntegral.Box.coe_eq_pi

added theorem BoxIntegral.Box.coe_inf

added theorem BoxIntegral.Box.coe_inj

added theorem BoxIntegral.Box.coe_mk'

added theorem BoxIntegral.Box.coe_ne_empty

added theorem BoxIntegral.Box.coe_subset_coe

added theorem BoxIntegral.Box.coe_subset_icc

added theorem BoxIntegral.Box.continuousOn_face_icc

added theorem BoxIntegral.Box.diam_icc_le_of_distortion_le

added theorem BoxIntegral.Box.disjoint_coe

added theorem BoxIntegral.Box.disjoint_withBotCoe

added theorem BoxIntegral.Box.dist_le_distortion_mul

added def BoxIntegral.Box.distortion

added theorem BoxIntegral.Box.distortion_eq_of_sub_eq_div

added theorem BoxIntegral.Box.empty_ne_coe

added theorem BoxIntegral.Box.exists_mem

added theorem BoxIntegral.Box.exists_seq_mono_tendsto

added theorem BoxIntegral.Box.ext

added def BoxIntegral.Box.face

added theorem BoxIntegral.Box.face_mk

added theorem BoxIntegral.Box.face_mono

added theorem BoxIntegral.Box.icc_def

added theorem BoxIntegral.Box.icc_eq_pi

added theorem BoxIntegral.Box.injective_coe

added theorem BoxIntegral.Box.ioo_subset_coe

added theorem BoxIntegral.Box.isSome_iff

added theorem BoxIntegral.Box.le_TFAE

added theorem BoxIntegral.Box.le_def

added theorem BoxIntegral.Box.le_iff_bounds

added theorem BoxIntegral.Box.le_iff_icc

added theorem BoxIntegral.Box.lower_le_upper

added theorem BoxIntegral.Box.lower_mem_icc

added theorem BoxIntegral.Box.lower_ne_upper

added theorem BoxIntegral.Box.mapsTo_insertNth_face

added theorem BoxIntegral.Box.mapsTo_insertNth_face_Icc

added theorem BoxIntegral.Box.mem_coe

added theorem BoxIntegral.Box.mem_def

added theorem BoxIntegral.Box.mem_mk

added theorem BoxIntegral.Box.mem_univ_Ioc

added def BoxIntegral.Box.mk'

added theorem BoxIntegral.Box.mk'_eq_bot

added theorem BoxIntegral.Box.mk'_eq_coe

added theorem BoxIntegral.Box.monotone_face

added theorem BoxIntegral.Box.monotone_upper

added theorem BoxIntegral.Box.ne_of_disjoint_coe

added theorem BoxIntegral.Box.nndist_le_distortion_mul

added theorem BoxIntegral.Box.nonempty_coe

added theorem BoxIntegral.Box.not_disjoint_coe_iff_nonempty_inter

added def BoxIntegral.Box.toSet

added theorem BoxIntegral.Box.unionᵢ_ioo_of_tendsto

added theorem BoxIntegral.Box.upper_mem

added theorem BoxIntegral.Box.upper_mem_icc

added theorem BoxIntegral.Box.withBotCoe_inj

added theorem BoxIntegral.Box.withBotCoe_subset_iff

added def BoxIntegral.Box.withBotToSet

added structure BoxIntegral.Box