finCons — Mathlib

English

If f is continuous at x and g is continuous at x, then the map a ↦ Fin.cons (f(a)) (g(a)) is continuous at x.

Русский

Если f непрерывна в точке x и g непрерывна в точке x, то a ↦ Fin.cons(f(a), g(a)) непрерывна в x.

LaTeX

$$$hf:\\text{ContinuousAt } f\\ x\\land hg:\\text{ContinuousAt } g\\ x\\Rightarrow \\text{ContinuousAt}(a\\mapsto \\mathrm{Fin.cons}(f(a), g(a)))\\ x$$$

Lean4

theorem finCons {f : X → A 0} {g : X → ∀ j : Fin n, A (Fin.succ j)} {x : X} (hf : ContinuousAt f x)
    (hg : ContinuousAt g x) : ContinuousAt (fun a => Fin.cons (f a) (g a)) x :=
  hf.tendsto.finCons hg

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