subsingleton_of_empty_left

Mathlib.LinearAlgebra.Matrix.Defs

URI: https://scilib.ai/kg/mathlib#Matrix.subsingleton_of_empty_left

English

If m is empty, then the matrix space over α is a singleton.

Русский

Если множество слева пустое, пространство матриц над α является единственным элементом.

LaTeX

$$$ IsEmpty(m) \\Rightarrow Subsingleton(Matrix(m,n,\\alpha)) $$$

Lean4

instance subsingleton_of_empty_left [IsEmpty m] : Subsingleton (Matrix m n α) :=
  ⟨fun M N => by
    ext i
    exact isEmptyElim i⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru