finSnoc — Mathlib

English

If f and g are continuous at a point x, then the pointwise snoc of f and g is also continuous at x.

Русский

Если f и g непрерывны в точке x, то точечное сложение (snoc) функций f и g также непрерывно в x.

LaTeX

$$$\\displaystyle \\text{ContinuousAt}\\bigl( a \\mapsto \\mathrm{Fin.snoc}( f(a), g(a) ) \\bigr)\\; x.$$$

Lean4

theorem finSnoc {f : X → ∀ j : Fin n, A j.castSucc} {g : X → A (Fin.last _)} {x : X} (hf : ContinuousAt f x)
    (hg : ContinuousAt g x) : ContinuousAt (fun a => Fin.snoc (f a) (g a)) x :=
  hf.tendsto.finSnoc hg

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