comp₄ — Mathlib

English

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

Русский

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

LaTeX

$$Continuous g → Continuous e → Continuous f → Continuous k → Continuous l → Continuous (λ w, g (e w, f w, k w, l 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) {l : W → ζ} (hl : Continuous l) :
    Continuous fun w => g (e w, f w, k w, l w) :=
  hg.comp₃ he hf <| hk.prodMk hl

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