isSupFiniteCompact_iff_all_elements_compact

English

A complete lattice α is Sup-Finite-Compact iff every element of α is compact.

Русский

Полная решётка α является суп-частичной (Sup-Finite-Compact), если и только если каждый элемент α компакт.

LaTeX

$$IsSupFiniteCompact α ↔ ∀ k : α, IsCompactElement k$$

Lean4

theorem isSupFiniteCompact_iff_all_elements_compact : IsSupFiniteCompact α ↔ ∀ k : α, IsCompactElement k :=
  by
  refine ⟨fun h k s hs => ?_, fun h s => ?_⟩
  · obtain ⟨t, ⟨hts, htsup⟩⟩ := h s
    use t, hts
    rwa [← htsup]
  · obtain ⟨t, ⟨hts, htsup⟩⟩ := h (sSup s) s (by rfl)
    have : sSup s = t.sup id :=
      by
      suffices t.sup id ≤ sSup s by apply le_antisymm <;> assumption
      simp only [id, Finset.sup_le_iff]
      intro x hx
      exact le_sSup _ _ (hts hx)
    exact ⟨t, hts, this⟩

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