comp₃ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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