cpolynomialOn — Mathlib

English

For a continuous linear map f and a set s, define CPolynomialOn 𝕜 f s as the family x ↦ cpolynomialAt 𝕜 f x; this gives a polynomial-valued function on s.

Русский

Для отображения f и множества s определим CPolynomialOn 𝕜 f s как x ↦ cpolynomialAt 𝕜 f x; это задаёт функцию-число на s, являющуюся полиномом.

LaTeX

$$$ CPolynomialOn 𝕜 f s = λ x ∈ s, cpolynomialAt 𝕜 f x $$$

Lean4

protected theorem cpolynomialOn (f : E →L[𝕜] F) (s : Set E) : CPolynomialOn 𝕜 f s := fun x _ ↦ f.cpolynomialAt x

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