Commit 2024-09-27 17:57 418c5378

View on Github →

feat: a few lemmas on WithTop ℕ∞ (#17164) To be used when WithTop ℕ∞ becomes the set of smoothness exponents, in #17152

Estimated changes

Modified Mathlib/Data/ENat/Basic.lean

added theorem ENat.add_one_eq_coe_top_iff

added theorem ENat.add_one_nat_le_withTop_of_lt

added theorem ENat.coe_top_add_one

added theorem ENat.nat_ne_coe_top

added theorem ENat.one_le_iff_ne_zero_withTop