continuous_map₂ — Mathlib

English

If a and b are continuous maps from δ to Completion α and Completion β, then d ↦ map₂ f (a d) (b d) is continuous.

Русский

Если a и b непрерывны как отображения из δ в Completion α и Completion β, то d ↦ map₂ f (a d) (b d) непрерывно.

LaTeX

$$$\\forall ha hb, \\ ha: Continuous a, hb: Continuous b \\implies Continuous\\; (d \\mapsto \\mathrm{Completion.map_2} f (a d) (b d))$$$

Lean4

theorem continuous_map₂ {δ} [TopologicalSpace δ] {f : α → β → γ} {a : δ → Completion α} {b : δ → Completion β}
    (ha : Continuous a) (hb : Continuous b) : Continuous fun d : δ => Completion.map₂ f (a d) (b d) :=
  cPkg.continuous_map₂ cPkg cPkg ha hb

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