contMDiff_iff_contDiff — Mathlib

English

A map between model-with-corners spaces is ContMDiff of order n iff it is ContDiff of order n globally (no manifold structure).

Русский

Отображение между моделями с углами является ContMDiff порядка n тогда и только тогда, когда оно гладко дифференцируемо порядка n в глобальном смысле.

LaTeX

$$$\ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f \iff \ContDiff 𝕜 n f$$$

Lean4

theorem contMDiff_iff_contDiff {f : E → E'} : ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, E') n f ↔ ContDiff 𝕜 n f := by
  rw [← contDiffOn_univ, ← contMDiffOn_univ, contMDiffOn_iff_contDiffOn]

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