contMDiffAt_iff_contDiffAt — Mathlib

English

For maps between normed spaces, ContMDiffWithinAt with modelWithCorners equals ContDiffWithinAt.

Русский

Для отображений между нормированными пространствами ContMDiffWithinAt с моделью с углами эквивалентен ContDiffWithinAt.

LaTeX

$$$\ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f s x \iff \ContDiffWithinAt 𝕜 n f s x$$$

Lean4

theorem contMDiffAt_iff_contDiffAt {f : E → E'} {x : E} : ContMDiffAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f x ↔ ContDiffAt 𝕜 n f x := by
  rw [← contMDiffWithinAt_univ, contMDiffWithinAt_iff_contDiffWithinAt, contDiffWithinAt_univ]

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