isCompactElement — Mathlib

English

If b ≤ a and b is compact in α, then b is compact as an element of the sublattice Iic(a).

Русский

Если b ≤ a и b компактный в α, то b компактный и в подпорядке Iic(a).

LaTeX

$$$ \text{IsCompactElement}(b) \Rightarrow \text{IsCompactElement}(b : Iic(a)) $$$

Lean4

theorem isCompactElement {a : α} {b : Iic a} (h : CompleteLattice.IsCompactElement (b : α)) :
    CompleteLattice.IsCompactElement b :=
  by
  simp only [CompleteLattice.isCompactElement_iff, Finset.sup_eq_iSup] at h ⊢
  intro ι s hb
  replace hb : (b : α) ≤ iSup ((↑) ∘ s) := le_trans hb <| (coe_iSup s) ▸ le_refl _
  obtain ⟨t, ht⟩ := h ι ((↑) ∘ s) hb
  exact ⟨t, (by simpa using ht : (b : α) ≤ _)⟩

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