instNeBotCoLindelofOfNonLindelofSpace

English

If X is non-Lindelöf, then Filter.coLindelof X is nontrivial (NeBot).

Русский

Если X не Линдельфово, то фильтр coLindelof X не тождественно пуст (NeBot).

LaTeX

$$$[NonLindelofSpace X] \Rightarrow (Filter.coLindelof X).NeBot$$$

Lean4

instance [NonLindelofSpace X] : NeBot (Filter.coLindelof X) :=
  by
  refine hasBasis_coLindelof.neBot_iff.2 fun {s} hs => ?_
  contrapose hs
  rw [not_nonempty_iff_eq_empty, compl_empty_iff] at hs
  rw [hs]
  exact nonLindelof_univ X

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