exists_seq_forall_of_frequently — Mathlib

English

If p frequently holds along l, there exists a sequence xs: ℕ → ι tending to l such that p holds for all indices n.

Русский

Если свойство p часто выполняется вдоль l, существует последовательность xs: ℕ → ι, сходящаяся к l, для которой p выполняется для каждого n.

LaTeX

$$$\\exists xs:\\mathbb{N} \\to ι, \\operatorname{Tendsto} xs\\ atTop\\ l \\land \\forall n, p (xs n)$$$

Lean4

theorem exists_seq_forall_of_frequently {ι : Type*} {l : Filter ι} {p : ι → Prop} [l.IsCountablyGenerated]
    (h : ∃ᶠ n in l, p n) : ∃ ns : ℕ → ι, Tendsto ns atTop l ∧ ∀ n, p (ns n) :=
  by
  rw [frequently_iff_seq_frequently] at h
  obtain ⟨x, hx_tendsto, hx_freq⟩ := h
  obtain ⟨n_to_n, h_tendsto, h_freq⟩ := subseq_forall_of_frequently hx_tendsto hx_freq
  exact ⟨x ∘ n_to_n, h_tendsto, h_freq⟩

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