instSubsingleton — Mathlib

English

If the left index type m is empty, then DMatrix m n α has at most one element.

Русский

Если left индекс типа m пуст, DMatrix m n α содержит хотя бы одно или ноль элементов, то есть subsingleton.

LaTeX

$$$[IsEmpty\\; m] \\Rightarrow \\operatorname{Subsingleton}(\\mathrm{DMatrix}\\, m\\, n\\, \\alpha)$$$

Lean4

instance [∀ i j, Subsingleton (α i j)] : Subsingleton (DMatrix m n α) :=
  inferInstanceAs <| Subsingleton <| ∀ i j, α i j

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