contMDiffOn_transContinuousLinearEquiv_right

English

The differentiability of a function under the transported model I.transContinuousLinearEquiv e is equivalent to its differentiability under the original model: contMDiff I' (I.transContinuousLinearEquiv e) n f ⇔ contMDiff I' I n f.

Русский

Гладкость функции после переноса модели эквивалентна гладкости функции в исходной модели.

LaTeX

$$$\mathrm{ContMDiff}\;I'\,(I.transContinuousLinearEquiv e)\;n\;f \;\Longleftrightarrow\; \mathrm{ContMDiff}\;I'\,I\;n\;f$$$

Lean4

@[simp]
theorem contMDiffOn_transContinuousLinearEquiv_right {f : M' → M} {s} :
    ContMDiffOn I' (I.transContinuousLinearEquiv e) n f s ↔ ContMDiffOn I' I n f s :=
  (toTransContinuousLinearEquiv I M e).contMDiffOn_diffeomorph_comp_iff le_rfl

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