hasBasis_coLindelof — Mathlib

English

The filter coLindelof has a basis consisting of complements of Lindelöf sets.

Русский

Фильтр coLindelof имеет базис из дополнений к Линдельоф-нам És.

LaTeX

$$$(coLindelof X).HasBasis (\lambda s, IsLindelof s) compl$$$

Lean4

theorem hasBasis_coLindelof : (coLindelof X).HasBasis IsLindelof compl :=
  hasBasis_biInf_principal'
    (fun s hs t ht =>
      ⟨s ∪ t, hs.union ht, compl_subset_compl.2 subset_union_left, compl_subset_compl.2 subset_union_right⟩)
    ⟨∅, isLindelof_empty⟩

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