nodup_append' — Mathlib

English

A variant of the nodup-append criterion: Nodup(l1 ++ l2) holds iff l1 and l2 are nodup and they are disjoint.

Русский

Вариант критерия безповторной конкатенации: Nodup(l1 ++ l2) эквивалентно тому, что l1 и l2 без повторов и они непересекаются.

LaTeX

$$$(l_1 ++ l_2).Nodup \\iff (l_1.Nodup \\land l_2.Nodup \\land \\operatorname{Disjoint}(l_1,l_2))$$$

Lean4

/-- This is a variant of the `nodup_append` from the standard library,
which does not use `Disjoint`. -/
theorem nodup_append' {l₁ l₂ : List α} : Nodup (l₁ ++ l₂) ↔ Nodup l₁ ∧ Nodup l₂ ∧ Disjoint l₁ l₂ := by
  simp only [Nodup, pairwise_append, disjoint_iff_ne]

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