Theorem Real.iInf_Ioi_eq_iInf_rat_gt

Modification history

2023-11-13 07:42

Mathlib/Data/Real/Archimedean.lean

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

Modified Real.iInf_Ioi_eq_iInf_rat_gt View on Github →

2023-08-14 12:01

Mathlib/Data/Real/Basic.lean

chore: move lemmas from Stietljes.lean to their proper afterport places (#6554)

Added Real.iInf_Ioi_eq_iInf_rat_gt View on Github →