derivWithin_fderivWithin — Mathlib

English

The linear map fderivWithin equals smulRight 1 applied to derivWithin f s x; equivalently, (fderivWithin 𝕜 f s x)(1) = derivWithin f s x.

Русский

Линейное отображение fderivWithin равно smulRight 1 применённому к derivWithin f s x; эквивалентно (fderivWithin 𝕜 f s x)(1) = derivWithin f s x.

LaTeX

$$$f\text{derivWithin } 𝕜 f s x = \mathrm{smulRight}(1)(\mathrm{derivWithin} f s x)$$$

Lean4

theorem derivWithin_fderivWithin : smulRight (1 : 𝕜 →L[𝕜] 𝕜) (derivWithin f s x) = fderivWithin 𝕜 f s x := by
  simp [derivWithin]

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