subtypeVal — Mathlib

English

There is a projection subtypeVal: Subtype_ p ⟹ α which extracts the underlying coordinate from a vector in Subtype_ p.

Русский

Существует отображение subtypeVal: Subtype_ p ⟹ α, извлекающее базовую координату из вектора в Subtype_ p.

LaTeX

$$$\\mathrm{subtypeVal} : \\mathrm{Subtype_} p \\Rightarrow α$$$

Lean4

/-- projection on `Subtype_` -/
def subtypeVal : ∀ {n} {α : TypeVec.{u} n} (p : α ⟹ «repeat» n Prop), Subtype_ p ⟹ α
  | succ n, _, _, Fin2.fs i => @subtypeVal n _ _ i
  | succ _, _, _, Fin2.fz => Subtype.val

Похожие утверждения