Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-27 20:45 38977584

View on Github →

feat(measure_theory): prove that more functions are measurable (#4266) Mostly additions to borel_space. Generalize measurable_bsupr and measurable_binfi to countable sets (instead of encodable underlying types). Use the lemma countable_encodable to get the original behavior. Some cleanup in borel_space: more instances are in variables, and lemmas with the same instances a bit more. One downside: there is a big import bump in borel_space, it currently imports hahn_banach. This is (only) used in measurable_smul_const. If someone has a proof sketch (in math) of measurable_smul_const that doesn't involve Hahn Banach (and that maybe generalizes real to a topological field or something), please let me know.

Estimated changes

modified theorem borel_eq_generate_Iio
modified theorem borel_eq_generate_Ioi
modified theorem is_measurable_interval
modified theorem is_measurable_le'
modified theorem is_measurable_le
modified theorem is_measurable_lt'
modified theorem is_measurable_lt
added theorem is_pi_system_is_open
modified theorem measurable.dist
modified theorem measurable.edist
modified theorem measurable.ennreal_add
modified theorem measurable.ennreal_coe
modified theorem measurable.ennreal_mul
modified theorem measurable.ennreal_of_real
modified theorem measurable.ennreal_sub
added theorem measurable.inf_dist
added theorem measurable.inf_edist
modified theorem measurable.is_glb
modified theorem measurable.is_lub
modified theorem measurable.max
modified theorem measurable.min
added theorem measurable.mul'
modified theorem measurable.nndist
modified theorem measurable.nnreal_coe
modified theorem measurable.nnreal_of_real
modified theorem measurable.sub_nnreal
added theorem measurable.to_nnreal
added theorem measurable.to_real
modified theorem measurable_binfi
modified theorem measurable_bsupr
added theorem measurable_cSup
modified theorem measurable_dist
modified theorem measurable_edist
added theorem measurable_ennnorm
added theorem measurable_inf_dist
added theorem measurable_inf_edist
modified theorem measurable_infi
modified theorem measurable_nndist
added theorem measurable_of_Ici
added theorem measurable_of_Iic
added theorem measurable_of_Iio
added theorem measurable_of_Ioi
added theorem measurable_of_is_open
added theorem measurable_smul_const
modified theorem measurable_supr
added theorem measurable_to_nnreal
added theorem nnreal.measurable_coe
added theorem is_measurable_swap_iff
added theorem measurable_prod
added theorem measurable_swap
added theorem measurable_swap_iff
added theorem is_closed_map_const