finCons — Mathlib

English

If f and g are continuous functions, then the combined map a ↦ Fin.cons (f(a)) (g(a)) is continuous.

Русский

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

LaTeX

$$$\\text{Continuous } f\\to\\text{Continuous } g \\Rightarrow \\text{Continuous}(a\\mapsto \\mathrm{Fin.cons}(f(a), g(a)))$$$

Lean4

theorem finCons {f : X → A 0} {g : X → ∀ j : Fin n, A (Fin.succ j)} (hf : Continuous f) (hg : Continuous g) :
    Continuous fun a => Fin.cons (f a) (g a) :=
  continuous_iff_continuousAt.2 fun _ => hf.continuousAt.finCons hg.continuousAt

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