Theorem Real.sInf_nonpos

Modification history

2024-10-02 17:17

Mathlib/Data/Real/Archimedean.lean

refactor(Data/Real/Archimedean): `sSup`/`sInf` API cleanup (#16735) …

Modified Real.sInf_nonpos View on Github →

2023-11-13 07:42

Mathlib/Data/Real/Archimedean.lean

chore: split Data.Real.Basic (#8356)

Modified Real.sInf_nonpos View on Github →

2023-05-14 07:05

Mathlib/Data/Real/Basic.lean

chore: Rename to `sSup`/`iSup` (#3938) …

Added Real.sInf_nonpos View on Github →