English
Let G be a structure groupoid on M with maximal atlas. If two open partial homeomorphisms e and e' are equivalent on their source (e' ≈ e) and e lies in the maximal atlas, then e' also lies in the maximal atlas.
Русский
Пусть G – структура-группоид на M с максимальным атласом. Если две частичные открытые гомоморфизмы e и e' эквивалентны по источнику (e' ≈ e) и e принадлежит максимальному атласу, то и e' принадлежит максимальному атласу.
LaTeX
$$$e' \approx e \land e \in G.maximalAtlas M \Rightarrow e' \in G.maximalAtlas M$$$
Lean4
/-- The maximal atlas of a structure groupoid is stable under equivalence. -/
theorem mem_maximalAtlas_of_eqOnSource {e e' : OpenPartialHomeomorph M H} (h : e' ≈ e) (he : e ∈ G.maximalAtlas M) :
e' ∈ G.maximalAtlas M := by
intro e'' he''
obtain ⟨l, r⟩ := mem_maximalAtlas_iff.mp he e'' he''
exact
⟨G.mem_of_eqOnSource l (EqOnSource.trans' (EqOnSource.symm' h) (e''.eqOnSource_refl)),
G.mem_of_eqOnSource r (EqOnSource.trans' (e''.symm).eqOnSource_refl h)⟩
