duplicate_cons_self_iff — Mathlib

English

Let α be a type, l a list of α, and x ∈ α. Then x appears at least twice in the list x :: l if and only if x occurs in l.

Русский

Пусть α — множество, l — список элементов α, и x — элемент α. Тогда x встречается как минимум дважды в списке x :: l тогда и только тогда, когда x встречается в l.

LaTeX

$$$\forall \alpha\, \forall l:\\ List\;\alpha\, \forall x:\ \alpha,\; x \in+ x \,::\, l \iff x \in l$$$

Lean4

@[simp]
theorem duplicate_cons_self_iff : x ∈+ x :: l ↔ x ∈ l :=
  ⟨Duplicate.mem_cons_self, Mem.duplicate_cons_self⟩

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