comp' — Mathlib

English

If g is continuous at f(x) and f is continuous at x, then the function x ↦ g(f(x)) is continuous at x.

Русский

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

LaTeX

$$$\\mathrm{ContinuousAt}(g, f(x)) \\Rightarrow \\mathrm{ContinuousAt}(f, x) \\Rightarrow \\mathrm{ContinuousAt}(\\lambda x. g(f(x)), x)$$$

Lean4

@[fun_prop]
theorem comp' {g : Y → Z} {x : X} (hg : ContinuousAt g (f x)) (hf : ContinuousAt f x) :
    ContinuousAt (fun x => g (f x)) x :=
  ContinuousAt.comp hg hf

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