English
Transport across equality of sets: given s=t, there is a natural equivalence between dependent functions on the subtype from s and on the subtype from t.
Русский
Перенос через равенство множеств: дано s=t, существует естественное эквив между зависимыми функциями на подтипе from s и на подтипе from t.
LaTeX
$$$\\text{piCongrSet}\\; (s=t): (\\forall i:\\{i\\mid i\\in s\\},W i)\\simeq (\\forall i:\\{i\\mid i\\in t\\},W i).$$$
Lean4
/-- Transport dependent functions through an equality of sets. -/
@[simps!]
def piCongrSet {α} {W : α → Sort w} {s t : Set α} (h : s = t) :
(∀ i : { i // i ∈ s }, W i) ≃ (∀ i : { i // i ∈ t }, W i)
where
toFun f i := f ⟨i, h ▸ i.2⟩
invFun f i := f ⟨i, h.symm ▸ i.2⟩
