Commit 2023-06-02 15:01 1cce5367

View on Github →

feat: port MeasureTheory.Measure.Lebesgue.Basic (#4552)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean

added theorem Filter.Eventually.volume_pos_of_nhds_real

added theorem Real.map_linearMap_volume_pi_eq_smul_volume_pi

added theorem Real.map_matrix_volume_pi_eq_smul_volume_pi

added theorem Real.map_volume_mul_left

added theorem Real.map_volume_mul_right

added theorem Real.smul_map_diagonal_volume_pi

added theorem Real.smul_map_volume_mul_left

added theorem Real.smul_map_volume_mul_right

added theorem Real.volume_Icc

added theorem Real.volume_Icc_pi

added theorem Real.volume_Icc_pi_toReal

added theorem Real.volume_Ici

added theorem Real.volume_Ico

added theorem Real.volume_Iic

added theorem Real.volume_Iio

added theorem Real.volume_Ioc

added theorem Real.volume_Ioi

added theorem Real.volume_Ioo

added theorem Real.volume_ball

added theorem Real.volume_closedBall

added theorem Real.volume_emetric_ball

added theorem Real.volume_emetric_closedBall

added theorem Real.volume_eq_stieltjes_id

added theorem Real.volume_interval

added theorem Real.volume_le_diam

added theorem Real.volume_pi_Ico

added theorem Real.volume_pi_Ico_toReal

added theorem Real.volume_pi_Ioc

added theorem Real.volume_pi_Ioc_toReal

added theorem Real.volume_pi_Ioo

added theorem Real.volume_pi_Ioo_toReal

added theorem Real.volume_pi_le_diam_pow

added theorem Real.volume_pi_le_prod_diam

added theorem Real.volume_preimage_mul_left

added theorem Real.volume_preimage_mul_right

added theorem Real.volume_preserving_transvectionStruct

added theorem Real.volume_singleton

added theorem Real.volume_univ

added theorem Real.volume_val

added theorem ae_of_mem_of_ae_of_mem_inter_Ioo

added theorem ae_restrict_of_ae_restrict_inter_Ioo

added theorem measurableSet_graph

added theorem measurableSet_regionBetween

added theorem measurableSet_region_between_cc

added theorem measurableSet_region_between_co

added theorem measurableSet_region_between_oc

added def regionBetween

added theorem regionBetween_subset

added theorem volume_regionBetween_eq_lintegral'

added theorem volume_regionBetween_eq_lintegral