English
The product of two C^n open partial homeomorphisms is C^n with respect to the product model I.prod I'.
Русский
Произведение двух C^n открытых частичных гомеоморфизмов имеет гладкость C^n относительно произведённой модели.
LaTeX
$$$e \in contDiffGroupoid\, n\, I$ and $e' \in contDiffGroupoid\, n\, I' \Rightarrow e.prod e' \in contDiffGroupoid\, n\, (I.prod I')$$$
Lean4
/-- The composition of an open partial homeomorphism from `H` to `M` and its inverse belongs to
the `C^n` groupoid. -/
theorem symm_trans_mem_contDiffGroupoid (e : OpenPartialHomeomorph M H) : e.symm.trans e ∈ contDiffGroupoid n I :=
haveI : e.symm.trans e ≈ OpenPartialHomeomorph.ofSet e.target e.open_target := OpenPartialHomeomorph.symm_trans_self _
StructureGroupoid.mem_of_eqOnSource _ (ofSet_mem_contDiffGroupoid e.open_target) this
