disjoint_of_nodup_append — Mathlib

English

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

Русский

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

LaTeX

$$$ \\operatorname{Nodup}(l_1 ++ l_2) \\rightarrow \\operatorname{Disjoint}(l_1,l_2) $$$

Lean4

theorem disjoint_of_nodup_append {l₁ l₂ : List α} (d : Nodup (l₁ ++ l₂)) : Disjoint l₁ l₂ :=
  (nodup_append'.1 d).2.2

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