finInsertNth — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem finInsertNth (i : Fin (n + 1)) {f : X → A i} {g : X → ∀ j : Fin n, A (i.succAbove j)} (hf : Continuous f)
    (hg : Continuous g) : Continuous fun a => i.insertNth (f a) (g a) :=
  continuous_iff_continuousAt.2 fun _ => hf.continuousAt.finInsertNth i hg.continuousAt

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