insert — Mathlib

English

If l is a nodup list, then inserting an element a yields a nodup list (assuming decidable equality).

Русский

Если список без повторов, то вставка элемента a дает список без повторов (при допустимой эквивалентности).

LaTeX

$$$ \\operatorname{Nodup}(l) \\Rightarrow \\operatorname{Nodup}(l\\,\\mathrm{insert}\\ a). $$$

Lean4

protected theorem insert [DecidableEq α] (h : l.Nodup) : (l.insert a).Nodup :=
  if h' : a ∈ l then by rw [insert_of_mem h']; exact h
  else by rw [insert_of_not_mem h', nodup_cons]; constructor <;> assumption

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