# Documentation

Mathlib.Data.Multiset.Nodup

# The Nodup predicate for multisets without duplicate elements. #

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

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

Equations
@[simp]
theorem Multiset.coe_nodup {α : Type u_1} {l : List α} :
@[simp]
theorem Multiset.nodup_zero {α : Type u_1} :
@[simp]
theorem Multiset.nodup_cons {α : Type u_1} {a : α} {s : } :
theorem Multiset.Nodup.cons {α : Type u_1} {s : } {a : α} (m : ¬a s) (n : ) :
@[simp]
theorem Multiset.nodup_singleton {α : Type u_1} (a : α) :
theorem Multiset.Nodup.of_cons {α : Type u_1} {s : } {a : α} (h : Multiset.Nodup (a ::ₘ s)) :
theorem Multiset.Nodup.not_mem {α : Type u_1} {s : } {a : α} (h : Multiset.Nodup (a ::ₘ s)) :
¬a s
theorem Multiset.nodup_of_le {α : Type u_1} {s : } {t : } (h : s t) :
theorem Multiset.nodup_iff_le {α : Type u_1} {s : } :
∀ (a : α), ¬a ::ₘ a ::ₘ 0 s
theorem Multiset.nodup_iff_ne_cons_cons {α : Type u_1} {s : } :
∀ (a : α) (t : ), s a ::ₘ a ::ₘ t
theorem Multiset.nodup_iff_count_le_one {α : Type u_1} [inst : ] {s : } :
∀ (a : α), 1
@[simp]
theorem Multiset.count_eq_one_of_mem {α : Type u_1} [inst : ] {a : α} {s : } (d : ) (h : a s) :
= 1
theorem Multiset.count_eq_of_nodup {α : Type u_1} [inst : ] {a : α} {s : } (d : ) :
= if a s then 1 else 0
theorem Multiset.nodup_iff_pairwise {α : Type u_1} {s : } :
Multiset.Pairwise (fun x x_1 => x x_1) s
theorem Multiset.Nodup.pairwise {α : Type u_1} {r : ααProp} {s : } :
((a : α) → a s(b : α) → b sa br a b) →
theorem Multiset.Pairwise.forall {α : Type u_1} {r : ααProp} {s : } (H : ) (hs : ) ⦃a : α :
a sb : α⦄ → b sa br a b
theorem Multiset.nodup_add {α : Type u_1} {s : } {t : } :
theorem Multiset.disjoint_of_nodup_add {α : Type u_1} {s : } {t : } (d : Multiset.Nodup (s + t)) :
theorem Multiset.Nodup.add_iff {α : Type u_1} {s : } {t : } (d₁ : ) (d₂ : ) :
theorem Multiset.Nodup.of_map {α : Type u_2} {β : Type u_1} {s : } (f : αβ) :
theorem Multiset.Nodup.map_on {α : Type u_1} {β : Type u_2} {s : } {f : αβ} :
(∀ (x : α), x s∀ (y : α), y sf x = f yx = y) →
theorem Multiset.Nodup.map {α : Type u_1} {β : Type u_2} {f : αβ} {s : } (hf : ) :
theorem Multiset.inj_on_of_nodup_map {α : Type u_1} {β : Type u_2} {f : αβ} {s : } :
∀ (x : α), x s∀ (y : α), y sf x = f yx = y
theorem Multiset.nodup_map_iff_inj_on {α : Type u_1} {β : Type u_2} {f : αβ} {s : } (d : ) :
∀ (x : α), x s∀ (y : α), y sf x = f yx = y
theorem Multiset.Nodup.filter {α : Type u_1} (p : αProp) [inst : ] {s : } :
@[simp]
theorem Multiset.nodup_attach {α : Type u_1} {s : } :
theorem Multiset.Nodup.pmap {α : Type u_1} {β : Type u_2} {p : αProp} {f : (a : α) → p aβ} {s : } {H : (a : α) → a sp a} (hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hba = b) :
instance Multiset.nodupDecidable {α : Type u_1} [inst : ] (s : ) :
Equations
theorem Multiset.Nodup.erase_eq_filter {α : Type u_1} [inst : ] (a : α) {s : } :
= Multiset.filter (fun x => x a) s
theorem Multiset.Nodup.erase {α : Type u_1} [inst : ] (a : α) {l : } :
theorem Multiset.Nodup.mem_erase_iff {α : Type u_1} [inst : ] {a : α} {b : α} {l : } (d : ) :
a a b a l
theorem Multiset.Nodup.not_mem_erase {α : Type u_1} [inst : ] {a : α} {s : } (h : ) :
theorem Multiset.Nodup.product {α : Type u_2} {β : Type u_1} {s : } {t : } :
Multiset.Nodup (s ×ˢ t)
theorem Multiset.Nodup.sigma {α : Type u_2} {s : } {σ : αType u_1} {t : (a : α) → Multiset (σ a)} :
(∀ (a : α), Multiset.Nodup (t a)) →
theorem Multiset.Nodup.filterMap {α : Type u_2} {β : Type u_1} {s : } (f : α) (H : ∀ (a a' : α) (b : β), b f ab f a'a = a') :
theorem Multiset.Nodup.inter_left {α : Type u_1} {s : } [inst : ] (t : ) :
Multiset.Nodup (s t)
theorem Multiset.Nodup.inter_right {α : Type u_1} {t : } [inst : ] (s : ) :
Multiset.Nodup (s t)
@[simp]
theorem Multiset.nodup_union {α : Type u_1} [inst : ] {s : } {t : } :
@[simp]
theorem Multiset.nodup_bind {α : Type u_1} {β : Type u_2} {s : } {t : α} :
(∀ (a : α), a sMultiset.Nodup (t a)) Multiset.Pairwise (fun a b => Multiset.Disjoint (t a) (t b)) s
theorem Multiset.Nodup.ext {α : Type u_1} {s : } {t : } :
→ (s = t ∀ (a : α), a s a t)
theorem Multiset.le_iff_subset {α : Type u_1} {s : } {t : } :
→ (s t s t)
theorem Multiset.range_le {m : } {n : } :
m n
theorem Multiset.mem_sub_of_nodup {α : Type u_1} [inst : ] {a : α} {s : } {t : } (d : ) :
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 : } {t : } (hs : ) (ht : ) (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 ta ha, b = i a ha) :
=