continuousLinearMapCoprod — Mathlib

English

If f and g are continuous on s, then the map x ↦ (f(x)).coprod (g(x)) is continuous on s.

Русский

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

LaTeX

$$$\text{If } f: X \to L(E,G),\ g: X \to L(F,G)\text{ are continuous on }s,\; x \mapsto (f(x)).coprod (g(x))\text{ is continuous on }s.$$$

Lean4

theorem continuousLinearMapCoprod {f : X → E →L[𝕜] G} {g : X → F →L[𝕜] G} {s : Set X} (hf : ContinuousOn f s)
    (hg : ContinuousOn g s) : ContinuousOn (fun x => (f x).coprod (g x)) s :=
  by
  simp only [← comp_fst_add_comp_snd]
  exact (hf.clm_comp continuousOn_const).add (hg.clm_comp continuousOn_const)

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