finTail — Mathlib

English

If f: Y → ∀ j : Fin (n+1), A j, then Fin.tail(f a) tends to Fin.tail x when f tends to x.

Русский

Если f сходится к x, тогда Fin.tail(f(a)) сходится к Fin.tail(x).

LaTeX

$$$\\displaystyle \\text{Tendsto}\\bigl( a \\mapsto \\mathrm{Fin.tail}( f(a) ) \\bigr)\\; l\\; \\mathcal{N}\\bigl( \\mathrm{Fin.tail}(x) \\bigr).$$$

Lean4

theorem finTail {f : Y → ∀ j : Fin (n + 1), A j} {l : Filter Y} {x : ∀ j, A j} (hg : Tendsto f l (𝓝 x)) :
    Tendsto (fun a ↦ Fin.tail (f a)) l (𝓝 <| Fin.tail x) :=
  tendsto_pi_nhds.2 fun j ↦ apply_nhds hg j.succ

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