sSup_compact_le_eq — Mathlib

English

In a compactly generated lattice, the supremum of a set of compact elements is the same as the supremum of all elements of that set.

Русский

В упоряженного образом: верхняя граница над множеством компактных элементов равна верхней границе над этим множеством.

LaTeX

$$sSup {c : α | CompleteLattice.IsCompactElement c ∧ c ≤ b} = b$$

Lean4

@[simp]
theorem sSup_compact_le_eq (b) : sSup {c : α | CompleteLattice.IsCompactElement c ∧ c ≤ b} = b :=
  by
  rcases IsCompactlyGenerated.exists_sSup_eq b with ⟨s, hs, rfl⟩
  exact le_antisymm (sSup_le fun c hc => hc.2) (sSup_le_sSup fun c cs => ⟨hs c cs, le_sSup cs⟩)

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