Theorem Nat.iSup_of_not_bddAbove

Modification history

2026-01-30 10:38
Mathlib/Data/Nat/Lattice.lean
feat(NNReal): supremum commutes with Nat.cast (#34467) …
Added Nat.iSup_of_not_bddAboveView on Github →