English
There is a diagonal-substitution map diagSub from α to α ⟹ Subtype_ repeatEq α, which uses the equality constraint to embed α into the subtype structure.
Русский
Существует диагональная подстановочная карта diagSub от α к α ⟹ Subtype_ repeatEq α, которая на основе равенства координат встраивает α в структуру подтипа.
LaTeX
$$$\\mathrm{diagSub} : α \\Rightarrow \\mathrm{Subtype_}(\\mathrm{repeatEq}\\ α)$$$
Lean4
/-- similar to `diag` but the target vector is a `Subtype_`
guaranteeing the equality of the components -/
def diagSub {n} {α : TypeVec.{u} n} : α ⟹ Subtype_ (repeatEq α)
| Fin2.fs _, x => @diagSub _ (drop α) _ x
| Fin2.fz, x => ⟨(x, x), rfl⟩
