Documentation

Mathlib.Data.Multiset.Nodup

The Nodup predicate for multisets without duplicate elements. #

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

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

Equations
Instances For
    @[simp]
    theorem Multiset.coe_nodup {α : Type u_1} {l : List α} :
    @[simp]
    @[simp]
    theorem Multiset.nodup_cons {α : Type u_1} {a : α} {s : Multiset α} :
    theorem Multiset.Nodup.cons {α : Type u_1} {s : Multiset α} {a : α} (m : as) (n : Multiset.Nodup s) :
    @[simp]
    theorem Multiset.nodup_singleton {α : Type u_1} (a : α) :
    theorem Multiset.Nodup.of_cons {α : Type u_1} {s : Multiset α} {a : α} (h : Multiset.Nodup (a ::ₘ s)) :
    theorem Multiset.Nodup.not_mem {α : Type u_1} {s : Multiset α} {a : α} (h : Multiset.Nodup (a ::ₘ s)) :
    as
    theorem Multiset.nodup_of_le {α : Type u_1} {s : Multiset α} {t : Multiset α} (h : s t) :
    theorem Multiset.not_nodup_pair {α : Type u_1} (a : α) :
    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
    theorem Multiset.nodup_iff_count_eq_one {α : Type u_1} {s : Multiset α} [DecidableEq α] :
    Multiset.Nodup s as, 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) :
    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 α} :
    (as, bs, a br a b)Multiset.Nodup sMultiset.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 sa br a b
    theorem Multiset.disjoint_of_nodup_add {α : Type u_1} {s : Multiset α} {t : Multiset α} (d : Multiset.Nodup (s + t)) :
    theorem Multiset.Nodup.add_iff {α : Type u_1} {s : Multiset α} {t : Multiset α} (d₁ : Multiset.Nodup s) (d₂ : Multiset.Nodup t) :
    theorem Multiset.Nodup.of_map {α : Type u_1} {β : Type u_2} {s : Multiset α} (f : αβ) :
    theorem Multiset.Nodup.map_on {α : Type u_1} {β : Type u_2} {s : Multiset α} {f : αβ} :
    (xs, ys, f x = f yx = y)Multiset.Nodup sMultiset.Nodup (Multiset.map f s)
    theorem Multiset.Nodup.map {α : Type u_1} {β : Type u_2} {f : αβ} {s : Multiset α} (hf : Function.Injective f) :
    theorem Multiset.nodup_map_iff_of_inj_on {α : Type u_1} {β : Type u_2} {s : Multiset α} {f : αβ} (d : xs, ys, f x = f yx = y) :
    theorem Multiset.nodup_map_iff_of_injective {α : Type u_1} {β : Type u_2} {s : Multiset α} {f : αβ} (d : Function.Injective f) :
    theorem Multiset.inj_on_of_nodup_map {α : Type u_1} {β : Type u_2} {f : αβ} {s : Multiset α} :
    Multiset.Nodup (Multiset.map f s)xs, ys, f x = f yx = 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) xs, ys, f x = f yx = y

    Alias of the reverse direction of Multiset.nodup_attach.

    theorem Multiset.Nodup.pmap {α : Type u_1} {β : Type u_2} {p : αProp} {f : (a : α) → p aβ} {s : Multiset α} {H : as, p a} (hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hba = b) :
    theorem Multiset.Nodup.erase_eq_filter {α : Type u_1} [DecidableEq α] (a : α) {s : Multiset α} :
    Multiset.Nodup sMultiset.erase s a = Multiset.filter (fun (x : α) => x a) s
    theorem Multiset.Nodup.erase {α : Type u_1} [DecidableEq α] (a : α) {l : Multiset α} :
    theorem Multiset.Nodup.mem_erase_iff {α : Type u_1} [DecidableEq α] {a : α} {b : α} {l : Multiset α} (d : Multiset.Nodup l) :
    theorem Multiset.Nodup.not_mem_erase {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} (h : Multiset.Nodup s) :
    aMultiset.erase s a
    theorem Multiset.Nodup.product {α : Type u_1} {β : Type u_2} {s : Multiset α} {t : Multiset β} :
    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' : α), bf a, b f a'a = a') :
    theorem Multiset.Nodup.inter_left {α : Type u_1} {s : Multiset α} [DecidableEq α] (t : Multiset α) :
    @[simp]
    theorem Multiset.nodup_bind {α : Type u_1} {β : Type u_2} {s : Multiset α} {t : αMultiset β} :
    Multiset.Nodup (Multiset.bind s t) (as, 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 sMultiset.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.mem_sub_of_nodup {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} {t : Multiset α} (d : Multiset.Nodup s) :
    a s - t a s at
    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) (i_inj : ∀ (a₁ : α) (ha₁ : a₁ s) (a₂ : α) (ha₂ : a₂ s), i a₁ ha₁ = i a₂ ha₂a₁ = a₂) (i_surj : bt, ∃ (a : α) (ha : a s), i a ha = b) (h : ∀ (a : α) (ha : a s), f a = g (i a ha)) :