contMDiffAt_transContinuousLinearEquiv_right

English

Similarly, ContMDiffAt is invariant under transporting the model: ContMDiffAt I' (I.transContinuousLinearEquiv e) n f x ⇔ ContMDiffAt I' I n f x.

Русский

Аналогично ContMDiffAt сохраняется при переносе модели: ContMDiffAt I' (I.transContinuousLinearEquiv e) n f x эквивалентно ContMDiffAt I' I n f x.

LaTeX

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

Lean4

@[simp]
theorem contMDiffAt_transContinuousLinearEquiv_right {f : M' → M} {x} :
    ContMDiffAt I' (I.transContinuousLinearEquiv e) n f x ↔ ContMDiffAt I' I n f x :=
  (toTransContinuousLinearEquiv I M e).contMDiffAt_diffeomorph_comp_iff le_rfl

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