Commit 2026-03-23 10:55 6682a4e7

View on Github →

feat(Order/ConditionallyCompleteLattice): sInf s ≤ sSup t for (s ∩ t).Nonempty (#35821)

Estimated changes

Modified Mathlib/Data/Real/Archimedean.lean

Modified Mathlib/Order/Bounds/Basic.lean

added theorem isGLB_le_isLUB_of_nonempty_inter

added theorem lowerBounds_le_upperBounds_of_nonempty_inter

Modified Mathlib/Order/CompleteLattice/Basic.lean

added theorem sInf_le_sSup_of_nonempty_inter

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

modified theorem csInf_le_csSup

added theorem csInf_le_csSup_of_nonempty_inter

modified theorem isGLB_csInf

modified theorem isLUB_csSup

Modified Mathlib/Topology/Order/Compact.lean