subsingleton0 — Mathlib

English

The 0-length type vector has at most one element: any two elements of TypeVec 0 are equal.

Русский

Вектор типа TypeVec 0 имеет не более одного элемента: любые два элемента TypeVec 0 равны между собой.

LaTeX

$$$$\\forall x,y \\in \\text{TypeVec}(0),\\ x = y.$$$$

Lean4

instance subsingleton0 : Subsingleton (TypeVec 0) :=
  ⟨fun _ _ => funext Fin2.elim0⟩
    -- See `Mathlib/Tactic/Attr/Register.lean` for `register_simp_attr typevec`

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