exists_seq_tendsto — Mathlib

English

If f is a nontrivial countably generated filter on α, then there exists a sequence x:ℕ→α with Tendsto x to f along atTop.

Русский

Если f — ненулевой счётно порожденный фильтр на α, существует последовательность x(n) такая, что x(n) стремится к f по atTop.

LaTeX

$$$$\exists x:\mathbb{N}\to \alpha\;\text{such that}\;\operatorname{Tendsto}(x, \text{atTop}, f).$$$$

Lean4

/-- If `f` is a nontrivial countably generated filter, then there exists a sequence that converges
to `f`. -/
theorem exists_seq_tendsto (f : Filter α) [IsCountablyGenerated f] [NeBot f] : ∃ x : ℕ → α, Tendsto x atTop f :=
  by
  obtain ⟨B, h⟩ := f.exists_antitone_basis
  choose x hx using fun n => Filter.nonempty_of_mem (h.mem n)
  exact ⟨x, h.tendsto hx⟩

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