comp — Mathlib

English

If g is continuous at y, f is continuous at x, and f(x) = y, then g ∘ f is continuous at x.

Русский

Если g непрерывна в y, f непрерывна в x, и f(x) = y, то g ∘ f непрерывна в x.

LaTeX

$$$\\mathrm{ContinuousAt}(g, y) \\rightarrow \\mathrm{ContinuousAt}(f, x) \\rightarrow f(x) = y \\rightarrow \\mathrm{ContinuousAt}(g \\circ f, x)$$$

Lean4

nonrec theorem comp {g : Y → Z} (hg : ContinuousAt g (f x)) (hf : ContinuousAt f x) : ContinuousAt (g ∘ f) x :=
  hg.comp hf

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