hasBasis_coclosedCompact — Mathlib

English

The coclosedCompact filter has a basis consisting of closed compact sets under complementation.

Русский

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

LaTeX

$$$(\operatorname{coclosedCompact}(X)).HasBasis (\lambda s. \operatorname{IsClosed}(s) \land \operatorname{IsCompact}(s)) \; \mathrm{compl}$$$

Lean4

theorem hasBasis_coclosedCompact : (Filter.coclosedCompact X).HasBasis (fun s => IsClosed s ∧ IsCompact s) compl :=
  by
  simp only [Filter.coclosedCompact, iInf_and']
  refine hasBasis_biInf_principal' ?_ ⟨∅, isClosed_empty, isCompact_empty⟩
  rintro s ⟨hs₁, hs₂⟩ t ⟨ht₁, ht₂⟩
  exact
    ⟨s ∪ t,
      ⟨⟨hs₁.union ht₁, hs₂.union ht₂⟩, compl_subset_compl.2 subset_union_left, compl_subset_compl.2 subset_union_right⟩⟩

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