mono

Mathlib.Analysis.Analytic.CPolynomialDef

URI: https://scilib.ai/kg/mathlib#CPolynomialOn.mono

English

If f is polynomial-on on t and s is contained in t, then f is polynomial-on on s.

Русский

Если f полином на множестве t и s ⊆ t, то f является полиномом на s.

LaTeX

$$$\forall s,t\subset E,\ CPolynomialOn 𝕜 f t \to (s \subset t) \Rightarrow CPolynomialOn 𝕜 f s.$$$

Lean4

theorem mono {s t : Set E} (hf : CPolynomialOn 𝕜 f t) (hst : s ⊆ t) : CPolynomialOn 𝕜 f s := fun z hz => hf z (hst hz)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru