nonempty_cauchyFilter_iff — Mathlib

English

Nonemptiness of the Cauchy filter space is equivalent to nonemptiness of the base space α.

Русский

Непустость пространства фильтров Коши эквивалентна непустости базового множества α.

LaTeX

$$$\\text{Nonempty}(\\mathrm{CauchyFilter}(\\alpha)) \\iff \\text{Nonempty}(\\alpha)$$$

Lean4

theorem nonempty_cauchyFilter_iff : Nonempty (CauchyFilter α) ↔ Nonempty α :=
  by
  constructor <;> rintro ⟨c⟩
  · have := eq_univ_iff_forall.1 isDenseEmbedding_pureCauchy.isDenseInducing.closure_range c
    obtain ⟨_, ⟨_, a, _⟩⟩ := mem_closure_iff.1 this _ isOpen_univ trivial
    exact ⟨a⟩
  · exact ⟨pureCauchy c⟩

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