closedUnderRestriction_idRestrGroupoid

English

A groupoid is closed under restriction if and only if it contains idRestrGroupoid.

Русский

Групоид замкнут по ограничению тогда и только тогда, когда он содержит idRestrGroupoid.

LaTeX

$$$ClosedUnderRestriction G \\iff idRestrGroupoid \\le G$$$

Lean4

/-- The trivial restriction-closed groupoid is indeed `ClosedUnderRestriction`. -/
instance closedUnderRestriction_idRestrGroupoid : ClosedUnderRestriction (@idRestrGroupoid H _) :=
  ⟨by
    rintro e ⟨s', hs', he⟩ s hs
    use s' ∩ s, hs'.inter hs
    refine Setoid.trans (OpenPartialHomeomorph.EqOnSource.restr he s) ?_
    exact ⟨by simp only [hs.interior_eq, mfld_simps], by simp only [mfld_simps, eqOn_refl]⟩⟩

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