continuous_map₂ — Mathlib

English

If a and b are continuous into hat spaces, then the map sending d to map₂ f (a d) (b d) is continuous.

Русский

Если a и b непрерывны в hat-пространства, то отображение d ↦ map₂ f (a d) (b d) непрерывно.

LaTeX

$$$ \text{Continuous } (fun d : \delta => pkg.map₂ pkg' pkg'' f (a d) (b d)) $$$

Lean4

theorem continuous_map₂ {δ} [TopologicalSpace δ] {f : α → β → γ} {a : δ → hatα} {b : δ → hatβ} (ha : Continuous a)
    (hb : Continuous b) : Continuous fun d : δ => pkg.map₂ pkg' pkg'' f (a d) (b d) :=
  (pkg.uniformContinuous_map₂ pkg' pkg'' f).continuous.comp₂ ha hb

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