English
MDifferentiableWithinAt 𝓘(𝕜,E) I' f s x ⇔ DifferentiableWithinAt 𝕜 f s x (self-source variant).
Русский
MDifferentiableWithinAt 𝓘(𝕜,E) I' f s x ⇔ DifferentiableWithinAt 𝕜 f s x (вариант с самим источником).
LaTeX
$$$ MDifferentiableWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') f s x \iff DifferentiableWithinAt 𝕜 f s x $$$
Lean4
/-- For maps between vector spaces, `mfderivWithin` and `fderivWithin` coincide -/
@[simp]
theorem mfderivWithin_eq_fderivWithin : mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f s x = fderivWithin 𝕜 f s x :=
by
by_cases h : MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x
· simp only [mfderivWithin, h, if_pos, mfld_simps]
· simp only [mfderivWithin, h, if_neg, not_false_iff]
rw [mdifferentiableWithinAt_iff_differentiableWithinAt] at h
exact (fderivWithin_zero_of_not_differentiableWithinAt h).symm
