Theorem NNReal.bddAbove_range_natCast_iff

Modification history

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