const_fin1_eq

Mathlib.Data.Fin.VecNotation

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

English

A constant function on Fin 1 is the one-element vector with that value.

Русский

Постоянная функция на Fin 1 равна одномерному вектору с этим значением.

LaTeX

$$$\\bigl( \\lambda \\_ : \\mathrm{Fin}(1), x \\bigr) = [x]$$$

Lean4

theorem const_fin1_eq (x : α) : (fun _ : Fin 1 => x) = ![x] :=
  (cons_fin_one x _).symm

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

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

Разделы

Аффилиация

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