compCM — Mathlib

English

The operation that sends a pair (f,g) ∈ C(X,Y) × C(Y,Z) to g ∘ f ∈ C(X,Z) is continuous (under appropriate conditions) — i.e., the composition map is continuous.

Русский

Операция (f,g) ↦ g ∘ f из C(X,Y) × C(Y,Z) в C(X,Z) непрерывна (при надлежащих условиях).

LaTeX

$$$\\text{Continuous}( (f,g) \\mapsto g\\circ f )$$$

Lean4

theorem _root_.Continuous.compCM (hg : Continuous g) (hf : Continuous f) : Continuous fun x => (g x).comp (f x) :=
  continuous_comp'.comp (hf.prodMk hg)

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