fun_comp_of_eq — Mathlib

English

Version of the polynomial composition at eq: if g is polynomial at y and f is polynomial at x, and f x = y, then the function z ↦ g (f z) is polynomial at x.

Русский

Версия композиции полиномов в точке уровнения: если g полином в y, f — полином в x, и f(x)=y, то z ↦ g(f(z)) полином в x.

LaTeX

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

Lean4

/-- Version of `CPolynomialAt.comp` where point equality is a separate hypothesis. -/
theorem fun_comp_of_eq {g : F → G} {f : E → F} {y : F} {x : E} (hg : CPolynomialAt 𝕜 g y) (hf : CPolynomialAt 𝕜 f x)
    (hy : f x = y) : CPolynomialAt 𝕜 (fun z ↦ g (f z)) x :=
  hg.comp_of_eq hf hy

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