Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-05 11:32 8d5830e6

View on Github →

chore(measure_theory/measurable_space): use implicit measurable_space argument (#11230) The measurable_space argument is inferred from other arguments (like measurable f or a measure for example) instead of being a type class. This ensures that the lemmas are usable without @ when several measurable space structures are used for the same type.

Estimated changes

modified theorem measurable.indicator
modified theorem measurable.ite
modified theorem measurable.piecewise
modified theorem measurable_from_top
modified theorem measurable_fst
modified theorem measurable_inl
modified theorem measurable_inr
modified theorem measurable_prod
modified theorem measurable_set_preimage
modified theorem measurable_set_range_inl
modified theorem measurable_set_range_inr
modified theorem measurable_snd
modified theorem measurable_swap
modified theorem measurable_swap_iff
modified theorem measurable_to_encodable
modified theorem measurable_unit
modified theorem subsingleton.measurable
modified theorem measurable.comp
modified theorem measurable_set.empty
modified def measurable_set