union — Mathlib

English

If l2 is nodup, then the union of an arbitrary list l1 with l2 is also nodup.

Русский

Если l2 без повторов, то объединение произвольного списка l1 с l2 также без повторов.

LaTeX

$$$ \\operatorname{Nodup}(l_2) \\Rightarrow \\operatorname{Nodup}(l_1 \\cup l_2). $$$

Lean4

theorem union [DecidableEq α] (l₁ : List α) (h : Nodup l₂) : (l₁ ∪ l₂).Nodup := by
  induction l₁ generalizing l₂ with
  | nil => exact h
  | cons a l₁ ih => exact (ih h).insert

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