fun_comp — Mathlib

English

If two functions g and f are continuously polynomial respectively at f x and x, then the function z ↦ g(f z) is continuously polynomial at x.

Русский

Если g и f непрерывно полиномальны в точках f(x) и x, то z ↦ g(f(z)) аналитически непрерывно полиномальна в x.

LaTeX

$$$CPolynomialAt 𝕜 g (f x) \\land CPolynomialAt 𝕜 f x \\Rightarrow CPolynomialAt 𝕜 (fun z => g (f z)) x$$$

Lean4

/-- If two functions `g` and `f` are continuously polynomial respectively at `f x` and `x`,
then `g ∘ f` is continuously polynomial at `x`. -/
theorem fun_comp {g : F → G} {f : E → F} {x : E} (hg : CPolynomialAt 𝕜 g (f x)) (hf : CPolynomialAt 𝕜 f x) :
    CPolynomialAt 𝕜 (fun z ↦ g (f z)) x :=
  hg.comp hf

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