ne_singleton — Mathlib

English

If x is duplicated in a list l, then l cannot be a singleton [y] for any y.

Русский

Если x встречается более одного раза в списке l, то l не может быть одиночным списком [y] для любого y.

LaTeX

$$$\forall \alpha\, \forall l:\ List\ \alpha\, \forall x:\alpha,\; x \in+ l \Rightarrow \forall y:\alpha,\; l \neq [y]$$$

Lean4

theorem ne_singleton (h : x ∈+ l) (y : α) : l ≠ [y] := by
  induction h with
  | cons_mem h => simp [ne_nil_of_mem h]
  | cons_duplicate h => simp [ne_nil_of_mem h.mem]

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