restrict — Mathlib

English

From a partial family of bijections on t, restricting to a smaller set s ⊆ t yields a partial family on s, induced by restriction of each component.

Русский

Из частичного семейства биекций на множесте t получить частичное семейство на меньшем множестве s ⊆ t путем ограничения каждого компонента.

LaTeX

$$$\\text{restrict} : \\mathrm{PEquivOn}(f, \\text{equivSucc}, t) \\to \\mathrm{PEquivOn}(f, \\text{equivSucc}, s)$$$

Lean4

/-- Restrict a partial family of bijections to a smaller set. -/
@[simps]
def restrict (e : PEquivOn f equivSucc t) (h : s ⊆ t) : PEquivOn f equivSucc s
    where
  equiv i := e.equiv ⟨i, h i.2⟩
  nat _ _ _ _ := e.nat _ _
  compat _ := e.compat _

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