finCons — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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