restrictScalars — Mathlib

English

If h is differentiable within s, then restricting scalars yields a differentiableWithinAt statement for h.

Русский

Если h дифференцируема внутри s, то ограничение скаляров даёт дифференцируемость внутри s для h.

LaTeX

$$$\text{DifferentiableWithinAt } 𝕜\, h\; s\; x \Rightarrow \text{DifferentiableWithinAt } 𝕜\; (h)\; s\; x$$$

Lean4

@[fun_prop]
theorem restrictScalars (h : DifferentiableWithinAt 𝕜' f s x) : DifferentiableWithinAt 𝕜 f s x :=
  (h.hasFDerivWithinAt.restrictScalars 𝕜).differentiableWithinAt

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