English
A groupoid is closed under restriction iff it contains the trivial restriction-closed groupoid.
Русский
Групоид замкнут по ограничению тогда и только тогда, когда он содержит тривиальный ограничено-закрытый группоид.
LaTeX
$$$ClosedUnderRestriction G \\iff idRestrGroupoid \\le G$$$
Lean4
/-- A groupoid is closed under restriction if and only if it contains the trivial restriction-closed
groupoid. -/
theorem closedUnderRestriction_iff_id_le (G : StructureGroupoid H) : ClosedUnderRestriction G ↔ idRestrGroupoid ≤ G :=
by
constructor
· intro _i
rw [StructureGroupoid.le_iff]
rintro e ⟨s, hs, hes⟩
refine G.mem_of_eqOnSource ?_ hes
convert closedUnderRestriction' G.id_mem hs
ext <;> simp [hs.interior_eq]
· intro h
constructor
intro e he s hs
rw [← ofSet_trans (e : OpenPartialHomeomorph H H) hs]
refine G.trans ?_ he
apply StructureGroupoid.le_iff.mp h
exact idRestrGroupoid_mem hs
