vec_single_eq_const

Mathlib.Data.Fin.VecNotation

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

English

The single-element vector ![a] is the constant function returning a.

Русский

Единичный вектор ![a] является константной функцией, возвращающей a.

LaTeX

$$$![a] = \lambda\_ : \mathrm{Fin}(1) \to \alpha, a$$$

Lean4

theorem vec_single_eq_const (a : α) : ![a] = fun _ => a :=
  let _ : Unique (Fin 1) := inferInstance
  funext <| Unique.forall_iff.2 rfl

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

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

Разделы

Аффилиация

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