Commit 2023-11-03 09:34 d8418cc7

View on Github →

feat(Data/Real/NNReal): add lemmas about Real.toNNReal (#8136) Add lemmas about comparison between Real.toNNReal and Nat.cast/OfNat.ofNat. Also add a few supporting lemmas.

Estimated changes

Modified Mathlib/Data/Nat/Cast/Defs.lean

added theorem Nat.AtLeastTwo.ne_one

added theorem Nat.AtLeastTwo.ne_zero

Modified Mathlib/Data/Real/NNReal.lean

added theorem Real.nat_cast_le_toNNReal'

added theorem Real.nat_cast_le_toNNReal

added theorem Real.nat_cast_lt_toNNReal

added theorem Real.ofNat_le_toNNReal

added theorem Real.ofNat_lt_toNNReal

added theorem Real.one_le_toNNReal

added theorem Real.one_lt_toNNReal

added theorem Real.toNNReal_eq_iff_eq_coe

added theorem Real.toNNReal_eq_nat_cast

added theorem Real.toNNReal_eq_ofNat

added theorem Real.toNNReal_eq_one

added theorem Real.toNNReal_le_nat_cast

added theorem Real.toNNReal_le_ofNat

added theorem Real.toNNReal_le_one

added theorem Real.toNNReal_le_toNNReal_iff'

added theorem Real.toNNReal_le_toNNReal_iff_of_pos

added theorem Real.toNNReal_lt_nat_cast'

added theorem Real.toNNReal_lt_nat_cast

added theorem Real.toNNReal_lt_ofNat

added theorem Real.toNNReal_lt_one