Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-10-25 21:55 3cd62290

View on Github →

refactor(analysis/real): use more coe instead of of_rat

Estimated changes

Modified analysis/ennreal.lean

Modified analysis/measure_theory/borel_space.lean

deleted theorem measure_theory.borel_eq_generate_from_Iio_of_rat

added theorem measure_theory.borel_eq_generate_from_Iio_rat

deleted theorem measure_theory.borel_eq_generate_from_Ioo_of_rat_of_rat

added theorem measure_theory.borel_eq_generate_from_Ioo_rat

deleted theorem measure_theory.is_topological_basis_Ioo_of_rat_of_rat

added theorem measure_theory.is_topological_basis_Ioo_rat

Modified analysis/measure_theory/lebesgue_measure.lean

Modified analysis/real.lean

deleted theorem exists_lt_of_rat_of_rat_gt

added theorem exists_lt_rat

added theorem exists_rat_btwn

added theorem exists_rat_lt

Modified data/int/basic.lean

added theorem int.cast_abs

added theorem int.cast_max

added theorem int.cast_min

Modified data/nat/cast.lean

added theorem nat.cast_max

added theorem nat.cast_min

Modified data/rat.lean

added theorem rat.cast_abs

added theorem rat.cast_max

added theorem rat.cast_min

Deleted data/subtype.lean

deleted theorem exists_subtype

deleted theorem forall_subtype