# mathlib3documentation

data.multiset.nodup

# The nodup predicate for multisets without duplicate elements. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
• s.nodup = multiset.nodup._proof_1
Instances for multiset.nodup
@[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 : multiset α} :
(a ::ₘ s).nodup a s s.nodup
theorem multiset.nodup.cons {α : Type u_1} {s : multiset α} {a : α} (m : a s) (n : s.nodup) :
(a ::ₘ s).nodup
@[simp]
theorem multiset.nodup_singleton {α : Type u_1} (a : α) :
{a}.nodup
theorem multiset.nodup.of_cons {α : Type u_1} {s : multiset α} {a : α} (h : (a ::ₘ s).nodup) :
theorem multiset.nodup.not_mem {α : Type u_1} {s : multiset α} {a : α} (h : (a ::ₘ s).nodup) :
a s
theorem multiset.nodup_of_le {α : Type u_1} {s t : multiset α} (h : s t) :
theorem multiset.not_nodup_pair {α : Type u_1} (a : α) :
theorem multiset.nodup_iff_le {α : Type u_1} {s : multiset α} :
s.nodup (a : α), ¬a ::ₘ a ::ₘ 0 s
theorem multiset.nodup_iff_ne_cons_cons {α : Type u_1} {s : multiset α} :
s.nodup (a : α) (t : multiset α), s a ::ₘ a ::ₘ t
theorem multiset.nodup_iff_count_le_one {α : Type u_1} [decidable_eq α] {s : multiset α} :
s.nodup (a : α), 1
@[simp]
theorem multiset.count_eq_one_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} (d : s.nodup) (h : a s) :
= 1
theorem multiset.count_eq_of_nodup {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} (d : s.nodup) :
= ite (a s) 1 0
theorem multiset.nodup_iff_pairwise {α : Type u_1} {s : multiset α} :
@[protected]
theorem multiset.nodup.pairwise {α : Type u_1} {r : α α Prop} {s : multiset α} :
( (a : α), a s (b : α), b s a b r a b) s.nodup
theorem multiset.pairwise.forall {α : Type u_1} {r : α α Prop} {s : multiset α} (H : symmetric r) (hs : s) ⦃a : α⦄ :
a s ⦃b : α⦄, b s a b r a b
theorem multiset.nodup_add {α : Type u_1} {s t : multiset α} :
theorem multiset.disjoint_of_nodup_add {α : Type u_1} {s t : multiset α} (d : (s + t).nodup) :
theorem multiset.nodup.add_iff {α : Type u_1} {s t : multiset α} (d₁ : s.nodup) (d₂ : t.nodup) :
(s + t).nodup s.disjoint 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 : α β} :
( (x : α), x s (y : α), y s f x = f y x = y) s.nodup s).nodup
theorem multiset.nodup.map {α : Type u_1} {β : Type u_2} {f : α β} {s : multiset α} (hf : function.injective f) :
theorem multiset.inj_on_of_nodup_map {α : Type u_1} {β : Type u_2} {f : α β} {s : multiset α} :
s).nodup (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 : s.nodup) :
s).nodup (x : α), x s (y : α), y s f x = f y x = y
theorem multiset.nodup.filter {α : Type u_1} (p : α Prop) {s : multiset α} :
@[simp]
theorem multiset.nodup_attach {α : Type u_1} {s : multiset α} :
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) :
s.nodup s H).nodup
@[protected, instance]
def multiset.nodup_decidable {α : Type u_1} [decidable_eq α] (s : multiset α) :
Equations
theorem multiset.nodup.erase_eq_filter {α : Type u_1} [decidable_eq α] (a : α) {s : multiset α} :
s.nodup s.erase a = multiset.filter (λ (_x : α), _x a) s
theorem multiset.nodup.erase {α : Type u_1} [decidable_eq α] (a : α) {l : multiset α} :
theorem multiset.nodup.mem_erase_iff {α : Type u_1} [decidable_eq α] {a b : α} {l : multiset α} (d : l.nodup) :
a l.erase b a b a l
theorem multiset.nodup.not_mem_erase {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} (h : s.nodup) :
a s.erase a
@[protected]
theorem multiset.nodup.product {α : Type u_1} {β : Type u_2} {s : multiset α} {t : multiset β} :
@[protected]
theorem multiset.nodup.sigma {α : Type u_1} {s : multiset α} {σ : α Type u_2} {t : Π (a : α), multiset (σ a)} :
s.nodup ( (a : α), (t a).nodup) (s.sigma t).nodup
@[protected]
theorem multiset.nodup.filter_map {α : Type u_1} {β : Type u_2} {s : multiset α} (f : α ) (H : (a a' : α) (b : β), b f a b f a' a = a') :
theorem multiset.nodup_range (n : ) :
theorem multiset.nodup.inter_left {α : Type u_1} {s : multiset α} [decidable_eq α] (t : multiset α) :
s.nodup (s t).nodup
theorem multiset.nodup.inter_right {α : Type u_1} {t : multiset α} [decidable_eq α] (s : multiset α) :
t.nodup (s t).nodup
@[simp]
theorem multiset.nodup_union {α : Type u_1} [decidable_eq α] {s t : multiset α} :
@[simp]
theorem multiset.nodup_bind {α : Type u_1} {β : Type u_2} {s : multiset α} {t : α } :
(s.bind t).nodup ( (a : α), a s (t a).nodup) multiset.pairwise (λ (a b : α), (t a).disjoint (t b)) s
theorem multiset.nodup.ext {α : Type u_1} {s t : multiset α} :
s.nodup t.nodup (s = t (a : α), a s a t)
theorem multiset.le_iff_subset {α : Type u_1} {s t : multiset α} :
s.nodup (s t s t)
theorem multiset.range_le {m n : } :
m n
theorem multiset.mem_sub_of_nodup {α : Type u_1} [decidable_eq α] {a : α} {s t : multiset α} (d : s.nodup) :
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 : s.nodup) (ht : t.nodup) (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 : a s), b = i a ha)) :
s = t