hasBasis_coclosedLindelof — Mathlib

English

The coclosedLindelof filter has a basis given by closed Lindelöf sets under complement.

Русский

Фильтр coclosedLindelof имеет базис из дополнений к замкнутым Линдельоф-множества.

LaTeX

$$$(Filter.coclosedLindelof X).HasBasis (fun s => IsClosed s \land IsLindelof s) compl$$$

Lean4

theorem hasBasis_coclosedLindelof : (Filter.coclosedLindelof X).HasBasis (fun s => IsClosed s ∧ IsLindelof s) compl :=
  by
  simp only [Filter.coclosedLindelof, iInf_and']
  refine hasBasis_biInf_principal' ?_ ⟨∅, isClosed_empty, isLindelof_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⟩⟩

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