continuous — Mathlib

English

If t is continuous and f is continuous, then x ↦ ϕ(t(x))(f(x)) is continuous.

Русский

Если t непрерывна и f непрерывна, то переход по потоку, фиксируя t и f, даёт непрерывную композицию.

LaTeX

$$$\text{Continuous } t \;\Rightarrow\; \text{Continuous } f \;\Rightarrow\; x \mapsto \varphi(t(x))(f(x)) \text{ is continuous}$$$

Lean4

@[continuity, fun_prop]
protected theorem continuous {β : Type*} [TopologicalSpace β] {t : β → τ} (ht : Continuous t) {f : β → α}
    (hf : Continuous f) : Continuous fun x => ϕ (t x) (f x) :=
  ϕ.cont'.comp (ht.prodMk hf)

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