English
If e,e' are charts in the atlas, then their transition e.symm ≫ₕ e' lies in G.
Русский
Если e и e' — карты атласа, то переход e^{-1} ≫ₕ e' принадлежит G.
LaTeX
$$$e.symm \; ≫ₕ \; e' \in G$ for $e,e' \in atlas H M$$$
Lean4
/-- If `G` is closed under restriction, the transition function between the restriction of two
charts `e` and `e'` lies in `G`. -/
theorem trans_restricted {e e' : OpenPartialHomeomorph M H} {G : StructureGroupoid H} (he : e ∈ atlas H M)
(he' : e' ∈ atlas H M) [HasGroupoid M G] [ClosedUnderRestriction G] {s : Opens M} (hs : Nonempty s) :
(e.subtypeRestr hs).symm ≫ₕ e'.subtypeRestr hs ∈ G :=
G.mem_of_eqOnSource (closedUnderRestriction' (G.compatible he he') (e.isOpen_inter_preimage_symm s.2))
(e.subtypeRestr_symm_trans_subtypeRestr hs e')
