finInsertNth — Mathlib

English

If f and g are continuous at x, then a ↦ i.insertNth (f a) (g a) is continuous at x.

Русский

Если f и g непрерывны в x, то a ↦ i.insertNth(f(a), g(a)) непрерывно в x.

LaTeX

$$$\\displaystyle \\text{ContinuousAt}\\bigl( a \\mapsto i.insertNth( f(a), g(a) ) \\bigr)\\; x.$$$

Lean4

theorem finInsertNth (i : Fin (n + 1)) {f : X → A i} {g : X → ∀ j : Fin n, A (i.succAbove j)} {x : X}
    (hf : ContinuousAt f x) (hg : ContinuousAt g x) : ContinuousAt (fun a => i.insertNth (f a) (g a)) x :=
  hf.tendsto.finInsertNth i hg

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