Theorem NNReal.bddAbove_natCast_image_iff

Modification history

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