range_cons_empty

Mathlib.Data.Fin.VecNotation

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

← MathLib Explorer

English

If u is the empty vector, then range(vecCons x u) equals {x}.

Русский

Если хвост пуст, то образ vecCons x u равен {x}.

LaTeX

$$$\mathrm{Set.range}(\mathrm{vecCons} x u) = \{ x \}$$$

Lean4

theorem range_cons_empty (x : α) (u : Fin 0 → α) : Set.range (Matrix.vecCons x u) = { x } := by
  rw [range_cons, range_empty, Set.union_empty]
    -- simp can prove this (up to commutativity)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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