uniqueMDiffWithinAt_iff_uniqueDiffWithinAt

English

MDifferentiableWithinAt is equivalent to differentiability within sets in the classical sense for Euclidean space under the canonical model.

Русский

MDifferentiableWithinAt эквивалентно обычной дифференцируемости внутри множеств в евклидовом пространстве под канонической моделью.

LaTeX

$$$\forall s,x,\; MDifferentiableWithinAt(I,I')(f,s,x) \iff \text{DifferentiableWithinAt}(f,s,x).$$$

Lean4

theorem uniqueMDiffWithinAt_iff_uniqueDiffWithinAt : UniqueMDiffWithinAt 𝓘(𝕜, E) s x ↔ UniqueDiffWithinAt 𝕜 s x := by
  simp only [UniqueMDiffWithinAt, mfld_simps]

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