English
Pi-types are equivalent to iterated products: there is a canonical equivalence between (∀ i, α i) and List.TProd α l, provided l is nodup and we have a membership witness h.
Русский
Типы-пи равны итеративным произведениям: существует каноническое эквивалентное соответствие между (∀ i, α i) и List.TProd α l при условии, что l неповторим и имеется доказательство принадлежности.
LaTeX
$$$\\mathrm{piEquivTProd} : (\\forall i, \\alpha i) \\simeq TProd \\alpha \\; l,$ при условиях $l.Nodup$ и соответствующих гипотезах.$$
Lean4
/-- Pi-types are equivalent to iterated products. -/
def piEquivTProd (hnd : l.Nodup) (h : ∀ i, i ∈ l) : (∀ i, α i) ≃ TProd α l :=
⟨TProd.mk l, TProd.elim' h, fun f => funext fun i => elim_mk l f (h i), mk_elim hnd h⟩
