fderivWithin_continuousAlternatingMap_apply_const_apply

English

Same as Const Apply with fderivWithin; the directional derivative relation holds.

Русский

То же самое для directional derivative внутри.

LaTeX

$$$\\forall hxs\\, hc\\, u\\, m:\\, (fderivWithin 𝕜 (λ y. (c(y))u) s x)\\, m = (fderivWithin 𝕜 c s x)\\, m\\, u.$$$

Lean4

/-- Application of a `ContinuousAlternatingMap` to a constant commutes with `fderivWithin`. -/
theorem fderivWithin_continuousAlternatingMap_apply_const_apply (hxs : UniqueDiffWithinAt 𝕜 s x)
    (hc : DifferentiableWithinAt 𝕜 c s x) (u : ι → F) (m : E) :
    (fderivWithin 𝕜 (fun y ↦ (c y) u) s x) m = (fderivWithin 𝕜 c s x) m u := by
  simp [fderivWithin_continuousAlternatingMap_apply_const hxs hc]

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