isSupClosedCompact — Mathlib

English

IsSupFiniteCompact α is equivalent to IsSupClosedCompact α for complete lattices.

Русский

Для полной решётки изобилия IsSupFiniteCompact эквивалентно IsSupClosedCompact.

LaTeX

$$IsSupFiniteCompact α ↔ IsSupClosedCompact α$$

Lean4

theorem isSupClosedCompact (h : IsSupFiniteCompact α) : IsSupClosedCompact α :=
  by
  intro s hne hsc; obtain ⟨t, ht₁, ht₂⟩ := h s; clear h
  rcases t.eq_empty_or_nonempty with h | h
  · subst h
    rw [Finset.sup_empty] at ht₂
    rw [ht₂]
    simp [eq_singleton_bot_of_sSup_eq_bot_of_nonempty ht₂ hne]
  · rw [ht₂]
    exact hsc.finsetSup_mem h ht₁

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