The Nodup predicate for multisets without duplicate elements.

def Multiset.Nodup {α : Type u_1} (s : Multiset α) : Prop

Nodup s means that s has no duplicates, i.e. the multiplicity of any element is at most 1.

Equations

• Multiset.Nodup s = Quot.liftOn s List.Nodup (_ : ∀ (x x_1 : List α), Setoid.r x x_1 → List.Nodup x = List.Nodup x_1)

@[simp]

theorem Multiset.coe_nodup {α : Type u_1} {l : List α} : Multiset.Nodup ↑l ↔ List.Nodup l

@[simp]

theorem Multiset.nodup_zero {α : Type u_1} : Multiset.Nodup 0

@[simp]

theorem Multiset.nodup_cons {α : Type u_1} {a : α} {s : Multiset α} : Multiset.Nodup (a ::ₘ s) ↔ ¬a ∈ s ∧ Multiset.Nodup s

theorem Multiset.Nodup.cons {α : Type u_1} {s : Multiset α} {a : α} (m : ¬a ∈ s) (n : Multiset.Nodup s) : Multiset.Nodup (a ::ₘ s)

@[simp]

theorem Multiset.nodup_singleton {α : Type u_1} (a : α) : Multiset.Nodup {a}

theorem Multiset.Nodup.of_cons {α : Type u_1} {s : Multiset α} {a : α} (h : Multiset.Nodup (a ::ₘ s)) : Multiset.Nodup s

theorem Multiset.Nodup.not_mem {α : Type u_1} {s : Multiset α} {a : α} (h : Multiset.Nodup (a ::ₘ s)) : ¬a ∈ s

theorem Multiset.nodup_of_le {α : Type u_1} {s : Multiset α} {t : Multiset α} (h : s ≤ t) : Multiset.Nodup t → Multiset.Nodup s

theorem Multiset.not_nodup_pair {α : Type u_1} (a : α) : ¬Multiset.Nodup (a ::ₘ a ::ₘ 0)

theorem Multiset.nodup_iff_le {α : Type u_1} {s : Multiset α} : Multiset.Nodup s ↔ ∀ (a : α), ¬a ::ₘ a ::ₘ 0 ≤ s

theorem Multiset.nodup_iff_ne_cons_cons {α : Type u_1} {s : Multiset α} : Multiset.Nodup s ↔ ∀ (a : α) (t : Multiset α), s ≠ a ::ₘ a ::ₘ t

theorem Multiset.nodup_iff_count_le_one {α : Type u_1} [DecidableEq α] {s : Multiset α} : Multiset.Nodup s ↔ ∀ (a : α), Multiset.count a s ≤ 1

@[simp]

theorem Multiset.count_eq_one_of_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} (d : Multiset.Nodup s) (h : a ∈ s) : Multiset.count a s = 1

theorem Multiset.count_eq_of_nodup {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} (d : Multiset.Nodup s) : Multiset.count a s = if a ∈ s then 1 else 0

theorem Multiset.nodup_iff_pairwise {α : Type u_4} {s : Multiset α} : Multiset.Nodup s ↔ Multiset.Pairwise (fun x x_1 => x ≠ x_1) s

theorem Multiset.Nodup.pairwise {α : Type u_1} {r : α → α → Prop} {s : Multiset α} : ((a : α) → a ∈ s → (b : α) → b ∈ s → a ≠ b → r a b) → Multiset.Nodup s → Multiset.Pairwise r s

theorem Multiset.Pairwise.forall {α : Type u_1} {r : α → α → Prop} {s : Multiset α} (H : Symmetric r) (hs : Multiset.Pairwise r s) ⦃a : α⦄ : a ∈ s → ⦃b : α⦄ → b ∈ s → a ≠ b → r a b

theorem Multiset.nodup_add {α : Type u_1} {s : Multiset α} {t : Multiset α} : Multiset.Nodup (s + t) ↔ Multiset.Nodup s ∧ Multiset.Nodup t ∧ Multiset.Disjoint s t

theorem Multiset.disjoint_of_nodup_add {α : Type u_1} {s : Multiset α} {t : Multiset α} (d : Multiset.Nodup (s + t)) : Multiset.Disjoint s t

theorem Multiset.Nodup.add_iff {α : Type u_1} {s : Multiset α} {t : Multiset α} (d₁ : Multiset.Nodup s) (d₂ : Multiset.Nodup t) : Multiset.Nodup (s + t) ↔ Multiset.Disjoint s t

theorem Multiset.Nodup.of_map {α : Type u_1} {β : Type u_2} {s : Multiset α} (f : α → β) : Multiset.Nodup (Multiset.map f s) → Multiset.Nodup s

theorem Multiset.Nodup.map_on {α : Type u_1} {β : Type u_2} {s : Multiset α} {f : α → β} : (∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y → x = y) → Multiset.Nodup s → Multiset.Nodup (Multiset.map f s)

theorem Multiset.Nodup.map {α : Type u_1} {β : Type u_2} {f : α → β} {s : Multiset α} (hf : Function.Injective f) : Multiset.Nodup s → Multiset.Nodup (Multiset.map f s)

theorem Multiset.inj_on_of_nodup_map {α : Type u_1} {β : Type u_2} {f : α → β} {s : Multiset α} : Multiset.Nodup (Multiset.map f s) → ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y → x = y

theorem Multiset.nodup_map_iff_inj_on {α : Type u_1} {β : Type u_2} {f : α → β} {s : Multiset α} (d : Multiset.Nodup s) : Multiset.Nodup (Multiset.map f s) ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y → x = y

theorem Multiset.Nodup.filter {α : Type u_1} (p : α → Prop) [DecidablePred p] {s : Multiset α} : Multiset.Nodup s → Multiset.Nodup (Multiset.filter p s)

@[simp]

theorem Multiset.nodup_attach {α : Type u_1} {s : Multiset α} : Multiset.Nodup (Multiset.attach s) ↔ Multiset.Nodup s

theorem Multiset.Nodup.pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {s : Multiset α} {H : (a : α) → a ∈ s → p a} (hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b) : Multiset.Nodup s → Multiset.Nodup (Multiset.pmap f s H)

instance Multiset.nodupDecidable {α : Type u_1} [DecidableEq α] (s : Multiset α) : Decidable (Multiset.Nodup s)

Equations

• Multiset.nodupDecidable s = Quotient.recOnSubsingleton s fun l => List.nodupDecidable l

theorem Multiset.Nodup.erase_eq_filter {α : Type u_1} [DecidableEq α] (a : α) {s : Multiset α} : Multiset.Nodup s → Multiset.erase s a = Multiset.filter (fun x => x ≠ a) s

theorem Multiset.Nodup.erase {α : Type u_1} [DecidableEq α] (a : α) {l : Multiset α} : Multiset.Nodup l → Multiset.Nodup (Multiset.erase l a)

theorem Multiset.Nodup.mem_erase_iff {α : Type u_1} [DecidableEq α] {a : α} {b : α} {l : Multiset α} (d : Multiset.Nodup l) : a ∈ Multiset.erase l b ↔ a ≠ b ∧ a ∈ l

theorem Multiset.Nodup.not_mem_erase {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} (h : Multiset.Nodup s) : ¬a ∈ Multiset.erase s a

theorem Multiset.Nodup.product {α : Type u_1} {β : Type u_2} {s : Multiset α} {t : Multiset β} : Multiset.Nodup s → Multiset.Nodup t → Multiset.Nodup (s ×ˢ t)

theorem Multiset.Nodup.sigma {α : Type u_1} {s : Multiset α} {σ : α → Type u_4} {t : (a : α) → Multiset (σ a)} : Multiset.Nodup s → (∀ (a : α), Multiset.Nodup (t a)) → Multiset.Nodup (Multiset.sigma s t)

theorem Multiset.Nodup.filterMap {α : Type u_1} {β : Type u_2} {s : Multiset α} (f : α → Option β) (H : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a') : Multiset.Nodup s → Multiset.Nodup (Multiset.filterMap f s)

theorem Multiset.nodup_range (n : ℕ) : Multiset.Nodup (Multiset.range n)

theorem Multiset.Nodup.inter_left {α : Type u_1} {s : Multiset α} [DecidableEq α] (t : Multiset α) : Multiset.Nodup s → Multiset.Nodup (s ∩ t)

theorem Multiset.Nodup.inter_right {α : Type u_1} {t : Multiset α} [DecidableEq α] (s : Multiset α) : Multiset.Nodup t → Multiset.Nodup (s ∩ t)

@[simp]

theorem Multiset.nodup_union {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} : Multiset.Nodup (s ∪ t) ↔ Multiset.Nodup s ∧ Multiset.Nodup t

@[simp]

theorem Multiset.nodup_bind {α : Type u_1} {β : Type u_2} {s : Multiset α} {t : α → Multiset β} : Multiset.Nodup (Multiset.bind s t) ↔ (∀ (a : α), a ∈ s → Multiset.Nodup (t a)) ∧ Multiset.Pairwise (fun a b => Multiset.Disjoint (t a) (t b)) s

theorem Multiset.Nodup.ext {α : Type u_1} {s : Multiset α} {t : Multiset α} : Multiset.Nodup s → Multiset.Nodup t → (s = t ↔ ∀ (a : α), a ∈ s ↔ a ∈ t)

theorem Multiset.le_iff_subset {α : Type u_1} {s : Multiset α} {t : Multiset α} : Multiset.Nodup s → (s ≤ t ↔ s ⊆ t)

theorem Multiset.range_le {m : ℕ} {n : ℕ} : Multiset.range m ≤ Multiset.range n ↔ m ≤ n

theorem Multiset.mem_sub_of_nodup {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} {t : Multiset α} (d : Multiset.Nodup s) : a ∈ s - t ↔ a ∈ s ∧ ¬a ∈ t

theorem Multiset.map_eq_map_of_bij_of_nodup {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → γ) (g : β → γ) {s : Multiset α} {t : Multiset β} (hs : Multiset.Nodup s) (ht : Multiset.Nodup t) (i : (a : α) → a ∈ s → β) (hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t) (h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)) (i_inj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) (i_surj : ∀ (b : β), b ∈ t → ∃ a ha, b = i a ha) : Multiset.map f s = Multiset.map g t