vecCons_const

Mathlib.Data.Fin.VecNotation

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

English

vecCons a (fun _ => a) is the constant function a on its domain.

Русский

vecCons a (функция, возвращающая a) задаёт константную функцию a на своём домене.

LaTeX

$$$\mathrm{vecCons} a (\lambda\_.a) = \lambda\_.a$$$

Lean4

theorem vecCons_const (a : α) : (vecCons a fun _ : Fin n => a) = fun _ => a :=
  funext <| Fin.forall_iff_succ.2 ⟨rfl, cons_val_succ _ _⟩

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

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

Разделы

Аффилиация

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