mdifferentiableOn_iff_differentiableOn

English

MDifferentiableOn 𝓘(𝕜,E) 𝓘(𝕜,E') f s is equivalent to DifferentiableOn 𝕜 f s.

Русский

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

LaTeX

$$$ MDifferentiableOn 𝓘(𝕜, E) 𝓘(𝕜, E') f s \iff DifferentiableOn 𝕜 f s $$$

Lean4

/-- For maps between vector spaces, `MDifferentiableOn` and `DifferentiableOn` coincide -/
theorem mdifferentiableOn_iff_differentiableOn : MDifferentiableOn 𝓘(𝕜, E) 𝓘(𝕜, E') f s ↔ DifferentiableOn 𝕜 f s := by
  simp only [MDifferentiableOn, DifferentiableOn, mdifferentiableWithinAt_iff_differentiableWithinAt]

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