not_countably_generated_nhds_infty_opc

English

The neighborhood filter at infinity in ℚ∞ is not countably generated.

Русский

Фильтр окрестностей в бесконечности ℚ∞ не счётно генерируем.

LaTeX

$$$\neg\operatorname{IsCountablyGenerated}(\mathcal{N}(\infty))$$$

Lean4

theorem not_countably_generated_nhds_infty_opc : ¬IsCountablyGenerated (𝓝 (∞ : ℚ∞)) :=
  by
  intro
  have : IsCountablyGenerated (comap (OnePoint.some : ℚ → ℚ∞) (𝓝 ∞)) := by infer_instance
  rw [OnePoint.comap_coe_nhds_infty, coclosedCompact_eq_cocompact] at this
  exact not_countably_generated_cocompact this

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