Commit 2026-09-22 12:37 9fe29c4b

View on Github →

feat(Order/CompactlyGenerated/Basic): the supremum of compact elements is compact and other basics (#42421)

⊥ is compact
⊔ of compacts is compact
WellFoundedGT implies that every element is compact
Generalize IsCompactlyGenerated to use IsLUB, like IsCompactElement & IsAtomistic

Estimated changes

Modified Mathlib/Algebra/Lie/Submodule.lean

Modified Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean

Modified Mathlib/LinearAlgebra/Span/Basic.lean

Modified Mathlib/Order/CompactlyGenerated/Basic.lean

deleted theorem CompleteLattice.isCompactlyGenerated_of_wellFoundedGT

added theorem IsBot.isCompactElement

added theorem IsCompactElement.of_wellFoundedGT

modified def IsCompactElement

added theorem IsCompactlyGenerated.exists_sSup_eq

added theorem IsCompactlyGenerated.of_wellFoundedGT

added theorem isCompactElement_congr

added theorem isLUB_setOfPred_le_and_isCompactElement

deleted theorem le_iff_compact_le_imp

added theorem le_iff_forall_isCompactElement

modified theorem sSup_compact_le_eq

Modified Mathlib/Order/CompactlyGenerated/Intervals.lean