English
The symmetrized transitive coordinate change coming from the oppositely oriented trivializations e and e' is continuously differentiable of class n on their common target set.
Русский
Переход координат между тривиализациями через симметрический сопряжённый переход гладок класса n.
LaTeX
$$$$\\text{ContMDiffOn }(e^{\\mathrm{symm}}\\!\\circ e'^{\\,-1})\\!\\text{ на }e\\text{-интервале}.$$$
Lean4
theorem contMDiffOn_symm_trans :
ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (e.toOpenPartialHomeomorph.symm ≫ₕ e'.toOpenPartialHomeomorph)
(e.target ∩ e'.target) :=
by
have Hmaps : MapsTo Prod.fst (e.target ∩ e'.target) (e.baseSet ∩ e'.baseSet) := fun x hx ↦
⟨e.mem_target.1 hx.1, e'.mem_target.1 hx.2⟩
rw [mapsTo_inter] at Hmaps
refine (contMDiffOn_fst.prodMk (contMDiffOn_fst.coordChange contMDiffOn_snd Hmaps.1 Hmaps.2)).congr ?_
rintro ⟨b, x⟩ hb
refine Prod.ext ?_ rfl
have : (e.toOpenPartialHomeomorph.symm (b, x)).1 ∈ e'.baseSet := by
simp_all only [Trivialization.mem_target, mfld_simps]
exact (e'.coe_fst' this).trans (e.proj_symm_apply hb.1)
