subsingleton_of_empty_right — Mathlib

English

If the right index type n is empty, then the matrix type DMatrix m n α is a singleton; in particular, any two matrices with right index n are equal.

Русский

Если множество индексов справа n пусто, то матрица DMatrix m n α имеет ровно один элемент; любые две такие матрицы равны.

LaTeX

$$$(n = \varnothing) \Rightarrow \lvert \mathrm{DMatrix}(m,n,\alpha) \rvert = 1$$$

Lean4

instance subsingleton_of_empty_right [IsEmpty n] : Subsingleton (DMatrix m n α) :=
  ⟨fun M N => by ext i j; exact isEmptyElim j⟩

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