instClosedUnderRestrictionContinuousGroupoid

English

The groupoid of open partial homeomorphisms is closed under restriction.

Русский

Групоид открытых частичных гомоморфизмов замкнут по ограничению.

LaTeX

$$$ClosedUnderRestriction(continuousGroupoid(H))$$$

Lean4

/-- The groupoid of all open partial homeomorphisms on a topological space `H`
is closed under restriction. -/
instance : ClosedUnderRestriction (continuousGroupoid H) :=
  (closedUnderRestriction_iff_id_le _).mpr le_top

Похожие утверждения