not_countably_generated_cocompact

English

The cocompact filter on ℚ is not countably generated.

Русский

Фильтр кокомпакт на ℚ не счётно генерируем.

LaTeX

$$$\neg\operatorname{IsCountablyGenerated}(\operatorname{cocompact}\mathbb{Q})$$$

Lean4

theorem not_countably_generated_cocompact : ¬IsCountablyGenerated (cocompact ℚ) :=
  by
  intro H
  rcases exists_seq_tendsto (cocompact ℚ ⊓ 𝓝 0) with ⟨x, hx⟩
  rw [tendsto_inf] at hx; rcases hx with ⟨hxc, hx0⟩
  obtain ⟨n, hn⟩ : ∃ n : ℕ, x n ∉ insert (0 : ℚ) (range x) :=
    (hxc.eventually hx0.isCompact_insert_range.compl_mem_cocompact).exists
  exact hn (Or.inr ⟨n, rfl⟩)

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