Theorem Real.sInf_neg

Modification history

2026-01-02 14:04
Mathlib/Data/Real/Archimedean.lean
feat: `stdPart x = sSup {r | r < x}` (#33007)
Added Real.sInf_negView on Github →