Commit 2026-01-15 22:57 26299a5a

View on Github →

refactor: generalise compact from CompleteLattice to PartialOrder (#33061) IsCompactElement assumes a CompleteLattice structure on the type for which it is defined. But a PartialOrder will suffice and this is the textbook definition of compact https://en.wikipedia.org/wiki/Compact_element. Also it is currently defined in a non-standard way. The standard definition uses directed sets. Changing this has indeed simplified most proofs by removing an rw into this more standard form.

Estimated changes

Modified Mathlib/Algebra/Lie/Submodule.lean

Modified Mathlib/LinearAlgebra/Span/Basic.lean

Modified Mathlib/Order/BooleanGenerators.lean

Modified Mathlib/Order/CompactlyGenerated/Basic.lean

deleted def CompleteLattice.IsCompactElement

deleted theorem CompleteLattice.isCompactElement_iff.{u}

added theorem CompleteLattice.isCompactElement_iff_exists_le_iSup_of_le_iSup.{u}

added theorem CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup

added def IsCompactElement

modified theorem sSup_compact_eq_top

Modified Mathlib/Order/CompactlyGenerated/Intervals.lean

modified theorem Set.Iic.isCompactElement

Modified Mathlib/RingTheory/Finiteness/Basic.lean

modified theorem Submodule.fg_iff_compact

Modified Mathlib/RingTheory/Ideal/Span.lean

modified theorem Ideal.isCompactElement_top

Modified Mathlib/RingTheory/Spectrum/Prime/Topology.lean

Modified Mathlib/Topology/Sets/Opens.lean