append — Mathlib

English

If l1 and l2 are nodup and disjoint, then their concatenation l1 ++ l2 is nodup.

Русский

Если l1 и l2 не содержат повторов и не пересекаются, то их конкатенация безповторна.

LaTeX

$$$(l_1.Nodup) \\land (l_2.Nodup) \\land (l_1 \\perp l_2) \\rightarrow \\operatorname{Nodup}(l_1 ++ l_2)$$$

Lean4

theorem append (d₁ : Nodup l₁) (d₂ : Nodup l₂) (dj : Disjoint l₁ l₂) : Nodup (l₁ ++ l₂) :=
  nodup_append'.2 ⟨d₁, d₂, dj⟩

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