nodup_union — Mathlib

English

Nodup (s ∪ t) holds if and only if Nodup s and Nodup t.

Русский

Nodup (s ∪ t) эквивалентно Nodup s и Nodup t.

LaTeX

$$Nodup (s ∪ t) \\iff Nodup s ∧ Nodup t$$

Lean4

@[simp]
theorem nodup_union [DecidableEq α] {s t : Multiset α} : Nodup (s ∪ t) ↔ Nodup s ∧ Nodup t :=
  ⟨fun h => ⟨nodup_of_le le_union_left h, nodup_of_le le_union_right h⟩, fun ⟨h₁, h₂⟩ =>
    nodup_iff_count_le_one.2 fun a => by
      rw [count_union]
      exact max_le (nodup_iff_count_le_one.1 h₁ a) (nodup_iff_count_le_one.1 h₂ a)⟩

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