finTail — Mathlib

English

If I is finite and each s(a) ∈ nhds(x(a)), then the product pi I s lies in nhds x.

Русский

Если I конечно, и для каждого a ∈ I s(a) лежит в nhds(x(a)), то pi I s ∈ nhds x.

LaTeX

$$$\\displaystyle \\text{pi } I\, s \\in \\mathcal{N}(x) \\quad\\text{given } I \\text{ finite and } s(a) \\in \\mathcal{N}(x(a)) \\text{ for all } a \\in I.$$$

Lean4

@[fun_prop]
theorem finTail {f : X → ∀ j : Fin (n + 1), A j} {x : X} (hf : ContinuousAt f x) :
    ContinuousAt (fun a ↦ Fin.tail (f a)) x :=
  hf.tendsto.finTail

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