contMDiffOn_model_symm — Mathlib

English

The inverse coordinate change map is smooth of order n.

Русский

Обратная карта перехода координат гладна порядка n.

LaTeX

$$$\mathrm{ContMDiffOn}\, 𝓘(\mathbb{C}, E)\ I\, n\, I^{-1}$$$

Lean4

theorem contMDiffOn_model_symm : ContMDiffOn 𝓘(𝕜, E) I n I.symm (range I) :=
  by
  rw [contMDiffOn_iff]
  refine ⟨I.continuousOn_symm, fun x y => ?_⟩
  simp only [mfld_simps]
  exact contDiffOn_id.congr fun x' => I.right_inv

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