English
If e is an open partial homeomorphism from M to H, then its symmetric composition e.symm.trans e lies in contDiffGroupoid.
Русский
Если e — открытое частичное гомеоморфизм M→H, то e.symm.trans e принадлежит contDiffGroupoid.
LaTeX
$$$e.symm.trans e \in contDiffGroupoid n I$$$
Lean4
/-- An identity open partial homeomorphism belongs to the `C^n` groupoid. -/
theorem ofSet_mem_contDiffGroupoid {s : Set H} (hs : IsOpen s) :
OpenPartialHomeomorph.ofSet s hs ∈ contDiffGroupoid n I :=
by
rw [contDiffGroupoid, mem_groupoid_of_pregroupoid]
suffices h : ContDiffOn 𝕜 n (I ∘ I.symm) (I.symm ⁻¹' s ∩ range I) by simp [h, contDiffPregroupoid]
have : ContDiffOn 𝕜 n id (univ : Set E) := contDiff_id.contDiffOn
exact this.congr_mono (fun x hx => I.right_inv hx.2) (subset_univ _)
