comp_of_eq — Mathlib

English

Version of the composition rule with point equality: if g is polynomial at y and f is polynomial at x, and f x = y, then g ∘ f is polynomial at x.

Русский

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

LaTeX

$$$CPolynomialAt 𝕜 g y \\land CPolynomialAt 𝕜 f x \\land f x = y \\Rightarrow CPolynomialAt 𝕜 (g \\circ f) x$$$

Lean4

/-- Version of `CPolynomialAt.comp` where point equality is a separate hypothesis. -/
theorem 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 𝕜 (g ∘ f) x := by
  rw [← hy] at hg
  exact hg.comp hf

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