vecCons_inj

Mathlib.Data.Fin.VecNotation

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

English

vecCons x u = vecCons y v if and only if x = y and u = v.

Русский

vecCons x u = vecCons y v тогда и только тогда, когда x = y и u = v.

LaTeX

$$$\mathrm{vecCons} x u = \mathrm{vecCons} y v \iff x = y \land u = v$$$

Lean4

@[simp]
theorem vecCons_inj {x y : α} {u v : Fin n → α} : vecCons x u = vecCons y v ↔ x = y ∧ u = v :=
  Fin.cons_inj

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

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

Разделы

Аффилиация

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