of_duplicate_cons

Mathlib.Data.List.Duplicate

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

English

If x appears duplicated in y :: l and x ≠ y, then x also appears duplicated in l.

Русский

Если x дублируется в y :: l и x ≠ y, тогда x также дублируется в l.

LaTeX

$$$(x \in+ y \:::\: l) \land x \neq y \Rightarrow x \in+ l$$$

Lean4

theorem of_duplicate_cons {y : α} (h : x ∈+ y :: l) (hx : x ≠ y) : x ∈+ l := by
  simpa [duplicate_cons_iff, hx.symm] using h

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

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

Разделы

Аффилиация

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