compCM — Mathlib

English

If X', a ∈ X', g: X' → C(Y, Z) and f: X' → C(X, Y) are such that g and f are continuous at a, then x ↦ (g(x) ∘ f(x)) is continuous at a.

Русский

Если g, f непрерывны в точке a, то x ↦ g(x) ∘ f(x) непрерывна в a.

LaTeX

$$$\\text{ContinuousAt}(a \\mapsto g(a)\\circ f(a))$ given $\\text{ContinuousAt}(g,a)$ and $\\text{ContinuousAt}(f,a)$$$

Lean4

nonrec theorem _root_.ContinuousAt.compCM (hg : ContinuousAt g a) (hf : ContinuousAt f a) :
    ContinuousAt (fun x ↦ (g x).comp (f x)) a :=
  hg.compCM hf

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