comp — Mathlib

English

If g is continuous and f is continuous, then g ∘ f is continuous.

Русский

Если g непрерывна и f непрерывна, то композиция g ∘ f непрерывна.

LaTeX

$$$\\mathrm{Continuous}(g) \\Rightarrow \\mathrm{Continuous}(f) \\Rightarrow \\mathrm{Continuous}(g \\circ f)$$$

Lean4

theorem comp {g : Y → Z} (hg : Continuous g) (hf : Continuous f) : Continuous (g ∘ f) :=
  continuous_def.2 fun _ h => (h.preimage hg).preimage hf

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