tendsto_atBot_of_eventually_const

English

If u: ι→X is eventually constant equal to x from some i0 onward with the opposite order, then u tends to x along atBot.

Русский

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

LaTeX

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

Lean4

theorem tendsto_atBot_of_eventually_const {ι : Type*} [Preorder ι] {u : ι → X} {i₀ : ι} (h : ∀ i ≤ i₀, u i = x) :
    Tendsto u atBot (𝓝 x) :=
  tendsto_atTop_of_eventually_const (ι := ιᵒᵈ) h

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