mdifferentiableAt_iff_differentiableAt

English

A map f is MDifferentiableAt 𝓘(𝕜,E) 𝓘(𝕜,E') at x iff f is DifferentiableAt 𝕜 at x.

Русский

Отображение f удовлетворяет MDifferentiableAt 𝓘(𝕜,E) 𝓘(𝕜,E') в точке x тогда и только тогда, когда оно дифференцируемо в классическом смысле в точке x.

LaTeX

$$$ MDifferentiableAt 𝓘(𝕜, E) 𝓘(𝕜, E') f x \iff DifferentiableAt 𝕜 f x $$$

Lean4

/-- For maps between vector spaces, `MDifferentiableAt` and `DifferentiableAt` coincide -/
theorem mdifferentiableAt_iff_differentiableAt : MDifferentiableAt 𝓘(𝕜, E) 𝓘(𝕜, E') f x ↔ DifferentiableAt 𝕜 f x :=
  by
  simp only [mdifferentiableAt_iff, differentiableWithinAt_univ, mfld_simps]
  exact ⟨fun H => H.2, fun H => ⟨H.continuousAt, H⟩⟩

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