English
The product of two C^n open partial homeomorphisms is C^n.
Русский
Произведение двух C^n открытых частичных гомеоморфизмов является C^n.
LaTeX
$$$contDiffGroupoid\; n\; I \ ; e \; prod \; e' \in contDiffGroupoid\; n\; (I.prod I')$$$
Lean4
/-- The product of two `C^n` open partial homeomorphisms is `C^n`. -/
theorem contDiffGroupoid_prod {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'}
{e : OpenPartialHomeomorph H H} {e' : OpenPartialHomeomorph H' H'} (he : e ∈ contDiffGroupoid n I)
(he' : e' ∈ contDiffGroupoid n I') : e.prod e' ∈ contDiffGroupoid n (I.prod I') :=
by
obtain ⟨he, he_symm⟩ := he
obtain ⟨he', he'_symm⟩ := he'
constructor <;> simp only [PartialEquiv.prod_source, OpenPartialHomeomorph.prod_toPartialEquiv, contDiffPregroupoid]
· have h3 := ContDiffOn.prodMap he he'
rw [← I.image_eq, ← I'.image_eq, prod_image_image_eq] at h3
rw [← (I.prod I').image_eq]
exact h3
· have h3 := ContDiffOn.prodMap he_symm he'_symm
rw [← I.image_eq, ← I'.image_eq, prod_image_image_eq] at h3
rw [← (I.prod I').image_eq]
exact h3
