restrict_scalars — Mathlib

English

If f is ContDiffAt 𝕜′ n at x, then f is ContDiffAt 𝕜 n at x after restricting scalars 𝕜.

Русский

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

LaTeX

$$$$\text{ContDiffAt}_{𝕜' } n f x \Rightarrow \text{ContDiffAt}_{𝕜} n f x.$$$$

Lean4

theorem restrict_scalars (h : ContDiffAt 𝕜' n f x) : ContDiffAt 𝕜 n f x :=
  contDiffWithinAt_univ.1 <| h.contDiffWithinAt.restrict_scalars _

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