English
There is a map ofSubtype' from Subtype_ p to a vector of subtypes indexed by Fin2 n, by taking the i-th coordinate’s element and embedding it as a pair via ofRepeat.
Русский
Существуют отображение ofSubtype' из Subtype_ p в вектор подтипов, индексируемых Fin2 n, берущего i-й элемент координаты и внедряющего его как пару через ofRepeat.
LaTeX
$$$\\mathrm{ofSubtype}' : (p : α \\Rightarrow \\mathrm{repeat}\\; n\\; \\mathrm{Prop}) \\Rightarrow \\mathrm{Subtype_} p \\Rightarrow (\\mathrm{Fun}\\; i:\\mathrm{Fin2}\,n) \\{ x : α_i \\times α_i \\mid \\mathrm{ofRepeat}(p i (\\mathrm{prod.mk} \\, i \\, x)) \\}$$$
Lean4
/-- similar to `of_subtype` adapted to relations (i.e. predicate on product) -/
def ofSubtype' {n} {α : TypeVec.{u} n} (p : α ⊗ α ⟹ «repeat» n Prop) :
Subtype_ p ⟹ fun i : Fin2 n => { x : α i × α i // ofRepeat <| p i (prod.mk _ x.1 x.2) }
| Fin2.fs i, x => ofSubtype' _ i x
| Fin2.fz, x => ⟨x.val, cast (by congr) x.property⟩
