mdifferentiableWithinAt_iff_differentiableWithinAt

English

MDifferentiableWithinAt 𝓘(𝕜,E) 𝓘(𝕜,E') f s x is equivalent to DifferentiableWithinAt 𝕜 f s x.

Русский

MDifferentiableWithinAt 𝓘(𝕜,E) 𝓘(𝕜,E') f s x эквивалентно DifferentiableWithinAt 𝕜 f s x.

LaTeX

$$$ MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x \iff DifferentiableWithinAt 𝕜 f s x $$$

Lean4

/-- For maps between vector spaces, `MDifferentiableWithinAt` and `DifferentiableWithinAt`
coincide -/
theorem mdifferentiableWithinAt_iff_differentiableWithinAt :
    MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x ↔ DifferentiableWithinAt 𝕜 f s x :=
  by
  simp only [mdifferentiableWithinAt_iff', mfld_simps]
  exact ⟨fun H => H.2, fun H => ⟨H.continuousWithinAt, H⟩⟩

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