empty_vecAlt1

Mathlib.Data.Fin.VecNotation

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

English

The alt1 of an empty vector is empty.

Русский

alt1 из пустого вектора равен пустому.

LaTeX

$$$\\text{vecAlt1} \\; h \\; (\\![] : Fin 0 → α) = \\![]$$$

Lean4

@[simp]
theorem empty_vecAlt1 (α) {h} : vecAlt1 h (![] : Fin 0 → α) = ![] := by simp [eq_iff_true_of_subsingleton]

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

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

Разделы

Аффилиация

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