isClosed_iff — Mathlib

English

Proof fragment relating membership in basic sets to ultrafilter structure.

Русский

Фрагмент доказательства, связывающий принадлежность базовым множествам с ультрафильтровой структурой.

LaTeX

$$$\\text{proof fragment}$$$

Lean4

theorem isClosed_iff {X : Compactum} (S : Set X) : IsClosed S ↔ ∀ F : Ultrafilter X, S ∈ F → X.str F ∈ S :=
  by
  rw [← isOpen_compl_iff]
  constructor
  · intro cond F h
    by_contra c
    specialize cond F c
    rw [compl_mem_iff_notMem] at cond
    contradiction
  · intro h1 F h2
    specialize h1 F
    rcases F.mem_or_compl_mem S with h | h
    exacts [absurd (h1 h) h2, h]

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