restrict_scalars — Mathlib

English

If f is ContDiffOn 𝕜′ n f s, then it is ContDiffOn 𝕜 n f s after restricting scalars 𝕜.

Русский

Если f имеет ContDiffOn 𝕜′ n на s, то после ограничения скаляров 𝕜 он остаётся ContDiffOn 𝕜 n на s.

LaTeX

$$$$\text{ContDiffOn}_{𝕜' } n f s \Rightarrow \text{ContDiffOn}_{𝕜} n f s.$$$$

Lean4

theorem restrict_scalars (h : ContDiffOn 𝕜' n f s) : ContDiffOn 𝕜 n f s := fun x hx => (h x hx).restrict_scalars _

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