range_cons

Mathlib.Data.Fin.VecNotation

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

← MathLib Explorer

English

The image of vecCons x u is the union of the singleton {x} with the image of u.

Русский

Образ vecCons x u равен объединению множества {x} и образа u.

LaTeX

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

Lean4

@[simp]
theorem range_cons (x : α) (u : Fin n → α) : Set.range (vecCons x u) = { x } ∪ Set.range u :=
  Set.ext fun y => by simp [Fin.exists_fin_succ, eq_comm]

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

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

Разделы

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

Аффилиация

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