sSup_compact_eq_top — Mathlib

English

In a compactly generated lattice, the supremum of compact elements equals the top element.

Русский

В компактно сгенерированной решётке верхняя грань над компактами равна вершине.

LaTeX

$$sSup_compact_eq_top$$

Lean4

@[simp]
theorem sSup_compact_eq_top : sSup {a : α | CompleteLattice.IsCompactElement a} = ⊤ :=
  by
  refine Eq.trans (congr rfl (Set.ext fun x => ?_)) (sSup_compact_le_eq ⊤)
  exact (and_iff_left le_top).symm

Похожие утверждения