contMDiffWithinAt_transContinuousLinearEquiv_right

English

For any f, s, and x, differentiability within a set with respect to the transported model I.transContinuousLinearEquiv e is equivalent to differentiability within the original model I: ContMDiffWithinAt I' (I.transContinuousLinearEquiv e) n f s x ⇔ ContMDiffWithinAt I' I n f s x.

Русский

Для любого f, множества s и точки x дифференцируемость внутри множества относительно преобразованной модели эквивалентна дифференцируемости относительно исходной модели.

LaTeX

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

Lean4

@[simp]
theorem contMDiffWithinAt_transContinuousLinearEquiv_right {f : M' → M} {x s} :
    ContMDiffWithinAt I' (I.transContinuousLinearEquiv e) n f s x ↔ ContMDiffWithinAt I' I n f s x :=
  (toTransContinuousLinearEquiv I M e).contMDiffWithinAt_diffeomorph_comp_iff le_rfl

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