Commit 2026-04-28 03:07 37edb68a

View on Github →

feat(Order/CompleteLattice/Defs): l ≤ sSup s ↔ in CompleteLinearOrder (#38439) ≤ theorems that match the existing b < sSup s ↔ and b < iSup f ↔ theorems. Also adds an sSup version of the existing CompleteLattice theorem iSup_lt_iff (iSup s < l ↔).

Estimated changes

deleted theorem iSup_eq_top
deleted theorem iSup_lt_iff
added theorem iSup_eq_top
added theorem iSup_lt_iff
added theorem le_iSup_iff_forall_lt
added theorem le_sSup_iff_forall_lt
modified theorem lt_iSup_iff
modified theorem sSup_eq_top
added theorem sSup_lt_iff
added theorem sSup_mem_upperBounds