finCons — Mathlib

English

If f and g are ContinuousWithinAt on s, then the finite concatenation Fin.cons(f, g) is ContinuousWithinAt on s.

Русский

Если f и g непрерывны внутри на s, то Fin.cons(f,g) непрерывна внутри на s.

LaTeX

$$$$\text{ContinuousWithinAt }f\ s\ a \land \text{ContinuousWithinAt }g\ s\ a \Rightarrow \text{ContinuousWithinAt }(\lambda a.\mathrm{Fin.cons}(f(a), g(a)))\ s\ a.$$$$

Lean4

theorem finCons {f : α → X 0} {g : α → ∀ j : Fin n, X (Fin.succ j)} {a : α} {s : Set α} (hf : ContinuousWithinAt f s a)
    (hg : ContinuousWithinAt g s a) : ContinuousWithinAt (fun a => Fin.cons (f a) (g a)) s a :=
  hf.tendsto.finCons hg

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