English
If two functions g and f are continuously polynomial respectively at f x and x, then g ∘ f is continuously polynomial at x.
Русский
Если функции g и f непрерывно полиномиальны в точке f(x) и x, то g ∘ f непрерывно полиномана в x.
LaTeX
$$$CPolynomialAt 𝕜 g (f x) \\land CPolynomialAt 𝕜 f x \\Rightarrow CPolynomialAt 𝕜 (g \\circ f) 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 comp {g : F → G} {f : E → F} {x : E} (hg : CPolynomialAt 𝕜 g (f x)) (hf : CPolynomialAt 𝕜 f x) :
CPolynomialAt 𝕜 (g ∘ f) x := by
rcases hg with ⟨q, m, hm⟩
rcases hf with ⟨p, n, hn⟩
refine ⟨q.comp p, m * (n + 1), ?_⟩
exact hm.comp (hn.of_le (Nat.le_succ n)) (Nat.zero_lt_succ n)
