finInit — Mathlib

English

If f: Y → ∀ j : Fin (n+1), A j, then Fin.init(f a) tends to Fin.init(x) along l whenever f tends to x along l.

Русский

Если f сходится к x по l, то Fin.init(f a) сходится к Fin.init(x) по l.

LaTeX

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

Lean4

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

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