English
Two open partial homeomorphs belong to the same structure groupoid iff they are equivalent on their source.
Русский
Две частичные открытые гомоморфизмы принадлежат одному структурному группоидам, если они эквивалентны на своих источниках.
LaTeX
$$e ∈ G ↔ e' ∈ G$$
Lean4
instance : InfSet (StructureGroupoid H) :=
⟨fun S =>
StructureGroupoid.mk (members := ⋂ s ∈ S, s.members) (trans' :=
by
simp only [mem_iInter]
intro e e' he he' i hi
exact i.trans' e e' (he i hi) (he' i hi)) (symm' :=
by
simp only [mem_iInter]
intro e he i hi
exact i.symm' e (he i hi)) (id_mem' := by
simp only [mem_iInter]
intro i _
exact i.id_mem') (locality' := by
simp only [mem_iInter]
intro e he i hi
refine i.locality' e ?_
intro x hex
rcases he x hex with ⟨s, hs⟩
exact ⟨s, ⟨hs.left, ⟨hs.right.left, hs.right.right i hi⟩⟩⟩) (mem_of_eqOnSource' :=
by
simp only [mem_iInter]
intro e e' he he'e
exact fun i hi => i.mem_of_eqOnSource' e e' (he i hi) he'e)⟩
