English
Given a vector α and a predicate-valued vector p, Subtype_ p denotes the type of vectors whose coordinates satisfy p coordinatewise.
Русский
Для вектора α и предикатов-переменных координат образуется множество Subtype_ p, состоящее из таких векторов, что каждая координата удовлетворяет соответствующему предикату.
LaTeX
$$$\\mathrm{Subtype_} : (α \\Rightarrow \\mathrm{repeat}\, n\\;\\mathrm{Prop}) \\to \\mathrm{TypeVec}\, n$$$
Lean4
/-- given a predicate vector `p` over vector `α`, `Subtype_ p` is the type of vectors
that contain an `α` that satisfies `p` -/
def Subtype_ : ∀ {n} {α : TypeVec.{u} n}, (α ⟹ «repeat» n Prop) → TypeVec n
| _, _, p, Fin2.fz => Subtype fun x => p Fin2.fz x
| _, _, p, Fin2.fs i => Subtype_ (dropFun p) i
