Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-08 00:45 68158304

View on Github →

chore(measure_theory/measure_space): add coe_fn instance

Estimated changes

Modified analysis/measure_theory/lebesgue_measure.lean

modified theorem measure_theory.lebesgue_Ico

modified theorem measure_theory.lebesgue_Ioo

modified theorem measure_theory.lebesgue_singleton

Modified analysis/measure_theory/measure_space.lean

modified theorem measure_theory.measure_Union_le_tsum_nat

modified theorem measure_theory.measure_empty

modified theorem measure_theory.measure_mono

modified theorem measure_theory.measure_space_eq