comp₂ — Mathlib

English

If g: X × Y → Z is continuous, e: W → X is continuous, f: W → Y is continuous, then w ↦ g(e(w), f(w)) is continuous.

Русский

Если g: X×Y→Z непрерывна, e:W→X непрерывна и f:W→Y непрерывна, то w↦g(e(w),f(w)) непрерывно на W.

LaTeX

$$Continuous g → Continuous e → Continuous f → Continuous (λ w, g (e w, f w))$$

Lean4

theorem comp₂ {g : X × Y → Z} (hg : Continuous g) {e : W → X} (he : Continuous e) {f : W → Y} (hf : Continuous f) :
    Continuous fun w => g (e w, f w) :=
  hg.comp <| he.prodMk hf

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