mem

Mathlib.Data.List.Duplicate

URI: https://scilib.ai/kg/mathlib#List.Duplicate.mem

English

From the duplicate relation, any element presumed in a duplicated structure belongs to the underlying list.

Русский

Из отношения дубликата следует, что элемент принадлежит базовому списку.

LaTeX

$$$$ \text{If } h: x \in^{+} l, \ x \in l. $$$$

Lean4

theorem mem (h : x ∈+ l) : x ∈ l := by
  induction h with
  | cons_mem => exact mem_cons_self
  | cons_duplicate _ hm => exact mem_cons_of_mem _ hm

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

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

Разделы

Аффилиация

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