English
If the family of sets of differences is locally finite, there exists a function F that stabilizes along the product of atTop and nhds x.
Русский
Если множество различий между последовательностями функциональных значений локально конечно, существует функция F, к которой последовательности сходятся в произведении фильтров atTop × 𝓝 x.
LaTeX
$$∃ F, ∀ x, ∀ᶠ p in atTop ×ˢ 𝓝 x, f p.1 p.2 = F p.2$$
Lean4
/-- Let `f : ℕ → α → β` be a sequence of functions on a topological space. Suppose
that the family of sets `s n = {x | f (n + 1) x ≠ f n x}` is locally finite. Then there exists a
function `F : α → β` such that for any `x`, for sufficiently large values of `n`, we have
`f n =ᶠ[𝓝 x] F`. -/
theorem exists_forall_eventually_atTop_eventuallyEq {f : ℕ → X → α}
(hf : LocallyFinite fun n => {x | f (n + 1) x ≠ f n x}) : ∃ F : X → α, ∀ x, ∀ᶠ n : ℕ in atTop, f n =ᶠ[𝓝 x] F :=
hf.exists_forall_eventually_atTop_eventually_eq'
