mem_of_mem_tail

Mathlib.Data.Vector.Mem

URI: https://scilib.ai/kg/mathlib#List.Vector.mem_of_mem_tail

← MathLib Explorer

English

If a is in the tail of v, then a is in v.

Русский

Если a принадлежит хвосту v, то a принадлежит v.

LaTeX

$$$$ a \in v.tail.toList \Rightarrow a \in v.toList $$$$

Lean4

theorem mem_of_mem_tail (v : Vector α n) (ha : a ∈ v.tail.toList) : a ∈ v.toList := by
  induction n with
  | zero => exact False.elim (Vector.notMem_zero a v.tail ha)
  | succ n _ => exact (mem_succ_iff a v).2 (Or.inr ha)

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

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

Разделы

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

Аффилиация

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