English
Compatibility of charts in the atlas is preserved by congruence of corresponding open partial homeomorphs.
Русский
Совместимость карт в атласе сохраняется под эквиваленцией соответствующих открытых частичных гомоморфизмов.
LaTeX
$$$\text{c.openPartialHomeomorph}(e,he) \;\cong\; \text{c.openPartialHomeomorph}(e',he')$ in the sense of structure-preserving equivalence.$$
Lean4
/-- Reformulate in the `StructureGroupoid` namespace the compatibility condition of charts in a
charted space admitting a structure groupoid, to make it more easily accessible with dot
notation. -/
theorem compatible {H : Type*} [TopologicalSpace H] (G : StructureGroupoid H) {M : Type*} [TopologicalSpace M]
[ChartedSpace H M] [HasGroupoid M G] {e e' : OpenPartialHomeomorph M H} (he : e ∈ atlas H M)
(he' : e' ∈ atlas H M) : e.symm ≫ₕ e' ∈ G :=
HasGroupoid.compatible he he'
