English
InfSet structure on StructureGroupoid defined by intersections of members.
Русский
Структура InfSet на StructureGroupoid задаётся через пересечение членов.
LaTeX
$$instInfSetStructureGroupoid H : InfSet (StructureGroupoid H)$$
Lean4
instance : Min (StructureGroupoid H) :=
⟨fun G G' =>
StructureGroupoid.mk (members := G.members ∩ G'.members) (trans' := fun e e' he he' =>
⟨G.trans' e e' he.left he'.left, G'.trans' e e' he.right he'.right⟩) (symm' := fun e he =>
⟨G.symm' e he.left, G'.symm' e he.right⟩) (id_mem' := ⟨G.id_mem', G'.id_mem'⟩) (locality' :=
by
intro e hx
apply (mem_inter_iff e G.members G'.members).mpr
refine And.intro (G.locality' e ?_) (G'.locality' e ?_)
all_goals
intro x hex
rcases hx x hex with ⟨s, hs⟩
use s
refine And.intro hs.left (And.intro hs.right.left ?_)
· exact hs.right.right.left
· exact hs.right.right.right) (mem_of_eqOnSource' := fun e e' he hee' =>
⟨G.mem_of_eqOnSource' e e' he.left hee', G'.mem_of_eqOnSource' e e' he.right hee'⟩)⟩
