tendsto_atTop_of_eventually_const

English

If u: ι→X is eventually constant equal to x from some i0 onward, then u tends to x along atTop.

Русский

Если последовательность u(i) становится равной x начиная с некоторого i0, то u стремится к x вдоль atTop.

LaTeX

$$$(\\forall i,\\ i \\ge i_0 \\Rightarrow u(i)=x) \\Rightarrow \\text{Tendsto } u\\ atTop\\ (\\mathcal{N}_x).$$$

Lean4

theorem tendsto_atTop_of_eventually_const {ι : Type*} [Preorder ι] {u : ι → X} {i₀ : ι} (h : ∀ i ≥ i₀, u i = x) :
    Tendsto u atTop (𝓝 x) :=
  Tendsto.congr' (EventuallyEq.symm ((eventually_ge_atTop i₀).mono h)) tendsto_const_nhds

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