restrictScalars — Mathlib

English

Restriction of scalars preserves AnalyticOn: if f is analytic on s for a larger field, it is analytic for the smaller field as well.

Русский

Ограничение скаляров сохраняет AnalyticOn: если f аналитична на s над большим полем, то аналитична и над меньшим полем.

LaTeX

$$$\mathrm{AnalyticOn}_{\mathbb{K}'}(f,s) \Rightarrow \mathrm{AnalyticOn}_{\mathbb{K}}(f,s)$$$

Lean4

theorem restrictScalars (hf : AnalyticOn 𝕜' f s) : AnalyticOn 𝕜 f s := fun x hx ↦ (hf x hx).restrictScalars

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