comp_cpolynomialOn — Mathlib

English

If f,g agree on an open set s, then f is polynomial-on s iff g is polynomial-on s.

Русский

Если f и g совпадают на открытом множестве s, то f полином на s тогда и только тогда, когда g полином на s.

LaTeX

$$IsOpen s → s.EqOn f g → (CPolynomialOn 𝕜 f s ↔ CPolynomialOn 𝕜 g s)$$

Lean4

/-- If a function `f` is continuously polynomial on a set `s` and `g` is a continuous linear map,
then `g ∘ f` is continuously polynomial on `s`. -/
theorem comp_cpolynomialOn {s : Set E} (g : F →L[𝕜] G) (h : CPolynomialOn 𝕜 f s) : CPolynomialOn 𝕜 (g ∘ f) s :=
  by
  rintro x hx
  rcases h x hx with ⟨p, n, r, hp⟩
  exact ⟨g.compFormalMultilinearSeries p, n, r, g.comp_hasFiniteFPowerSeriesOnBall hp⟩

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