finSnoc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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