comp₂ — Mathlib

English

If f is continuous at (g x, h x), and g and h are continuous at x, then the composition x ↦ f (g x, h x) is continuous at x.

Русский

Если f непрерывна в (g x, h x), а g и h непрерывны в x, то композиция x ↦ f(g x, h x) непрерывна в x.

LaTeX

$$$ (ContinuousAt f (g x, h x)) \\land (ContinuousAt g x) \\land (ContinuousAt h x) \\Rightarrow ContinuousAt (\\\\lambda x. f (g x, h x)) x $$$

Lean4

theorem comp₂ {f : Y × Z → W} {g : X → Y} {h : X → Z} {x : X} (hf : ContinuousAt f (g x, h x)) (hg : ContinuousAt g x)
    (hh : ContinuousAt h x) : ContinuousAt (fun x ↦ f (g x, h x)) x :=
  ContinuousAt.comp hf (hg.prodMk hh)

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