English
There is a mapping toSubtype from a predicate vector p to a vector of subtypes, giving for each i the i-th coordinate of the subtype.
Русский
Существует отображение toSubtype от вектора предикатов к вектору подтипов, где i-я координата задается соответствующим подтипом.
LaTeX
$$$\\mathrm{toSubtype} : (p : α \\Rightarrow \\mathrm{repeat}\\; n\\; \\mathrm{Prop}) \\Rightarrow \\mathrm{TypeVec}\\, n \\to \\mathrm{Subtype_} p$$$
Lean4
/-- arrow that rearranges the type of `Subtype_` to turn a subtype of vector into
a vector of subtypes -/
def toSubtype :
∀ {n} {α : TypeVec.{u} n} (p : α ⟹ «repeat» n Prop), (fun i : Fin2 n => { x // ofRepeat <| p i x }) ⟹ Subtype_ p
| succ _, _, p, Fin2.fs i, x => toSubtype (dropFun p) i x
| succ _, _, _, Fin2.fz, x => x
