Theorem unionᵢ_Ioo_of_mono_of_isGLB_of_isLUB

Modification history

2023-05-14 07:05

Mathlib/Data/Set/Intervals/Monotone.lean

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

Deleted unionᵢ_Ioo_of_mono_of_isGLB_of_isLUB View on Github →

2023-01-03 02:50

Mathlib/Data/Set/Intervals/Monotone.lean

feat: port Data.Set.Intervals.Monotone (#1294) …

Added unionᵢ_Ioo_of_mono_of_isGLB_of_isLUB View on Github →