contMDiff_model — Mathlib

English

The identity transformation on the model with corners is smooth of order n.

Русский

Идентичность на модели с углами гладна порядка n.

LaTeX

$$$\mathrm{ContMDiff}\, I\, 𝓘(\mathbb{C}, E)\, n\, I$$$

Lean4

theorem contMDiff_model : ContMDiff I 𝓘(𝕜, E) n I := by
  intro x
  refine contMDiffAt_iff.mpr ⟨I.continuousAt, ?_⟩
  simp only [mfld_simps]
  refine contDiffWithinAt_id.congr_of_eventuallyEq ?_ ?_
  · exact Filter.eventuallyEq_of_mem self_mem_nhdsWithin fun x₂ => I.right_inv
  simp_rw [Function.comp_apply, I.left_inv, Function.id_def]

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