zero_subsingleton — Mathlib

English

The empty vector space of length 0 is a subsingleton: any two zero-length vectors are equal.

Русский

Пусть длина вектора нулевая; множество пустых векторов является пододномарфным: любые два нулевых вектора равны.

LaTeX

$$$\\mathrm{Subsingleton}(\\mathrm{Vector}(\\alpha,0))$$$

Lean4

/-- The empty `Vector` is a `Subsingleton`. -/
instance zero_subsingleton : Subsingleton (Vector α 0) :=
  ⟨fun _ _ => Vector.ext fun m => Fin.elim0 m⟩

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