prod_mapL — Mathlib

English

A root-level statement that prodMapL respects equivalences via continuous maps.

Русский

Корневое утверждение о том, что prodMapL сохраняет эквивалентности через непрерывные отображения.

LaTeX

$$$$\\text{prodMapL}^{{-1}}(f, g) = f \\times g.$$$$

Lean4

theorem _root_.ContinuousOn.prod_mapL {f : X → M₁ →L[𝕜] M₂} {g : X → M₃ →L[𝕜] M₄} {s : Set X} (hf : ContinuousOn f s)
    (hg : ContinuousOn g s) : ContinuousOn (fun x => (f x).prodMap (g x)) s :=
  ((prodMapL 𝕜 M₁ M₂ M₃ M₄).continuous.comp_continuousOn (hf.prodMk hg) :)

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