mathlib documentation

data.multiset.nodup

The nodup predicate for multisets without duplicate elements.

source
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
source
@[simp]
theorem multiset.coe_nodup {α : Type u_1} {l : list α} :
↑l.nodup ↔ l.nodup

source
@[simp]
theorem multiset.nodup_zero {α : Type u_1} :
0.nodup

source
@[simp]
theorem multiset.nodup_cons {α : Type u_1} {a : α} {s : multiset α} :
(a :: s).nodup ↔ a ∉ s ∧ s.nodup

source
theorem multiset.nodup_cons_of_nodup {α : Type u_1} {a : α} {s : multiset α} (m : a ∉ s) (n : s.nodup) :
(a :: s).nodup

source
theorem multiset.nodup_singleton {α : Type u_1} (a : α) :
(a :: 0).nodup

source
theorem multiset.nodup_of_nodup_cons {α : Type u_1} {a : α} {s : multiset α} (h : (a :: s).nodup) :
s.nodup

source
theorem multiset.not_mem_of_nodup_cons {α : Type u_1} {a : α} {s : multiset α} (h : (a :: s).nodup) :
a ∉ s

source
theorem multiset.nodup_of_le {α : Type u_1} {s t : multiset α} (h : s ≤ t) (a : t.nodup) :
s.nodup

source
theorem multiset.not_nodup_pair {α : Type u_1} (a : α) :
¬(a :: a :: 0).nodup

source
theorem multiset.nodup_iff_le {α : Type u_1} {s : multiset α} :
s.nodup ↔ ∀ (a : α), ¬a :: a :: 0 ≤ s

source
theorem multiset.nodup_iff_ne_cons_cons {α : Type u_1} {s : multiset α} :
s.nodup ↔ ∀ (a : α) (t : multiset α), s ≠ a :: a :: t

source
theorem multiset.nodup_iff_count_le_one {α : Type u_1} [decidable_eq α] {s : multiset α} :
s.nodup ↔ ∀ (a : α), multiset.count a s ≤ 1

source
@[simp]
theorem multiset.count_eq_one_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} (d : s.nodup) (h : a ∈ s) :
multiset.count a s = 1

source
theorem multiset.nodup_iff_pairwise {α : Type u_1} {s : multiset α} :
s.nodup ↔ multiset.pairwise ne s

source
theorem multiset.pairwise_of_nodup {α : Type u_1} {r : α → α → Prop} {s : multiset α} (a : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ≠ b → r a b) (a_1 : s.nodup) :
multiset.pairwise r s

source
theorem multiset.forall_of_pairwise {α : Type u_1} {r : α → α → Prop} (H : symmetric r) {s : multiset α} (hs : multiset.pairwise r s) (a : α) (H_1 : a ∈ s) (b : α) (H_2 : b ∈ s) (a_1 : a ≠ b) :
r a b

source
theorem multiset.nodup_add {α : Type u_1} {s t : multiset α} :
(s + t).nodup ↔ s.nodup ∧ t.nodup ∧ s.disjoint t

source
theorem multiset.disjoint_of_nodup_add {α : Type u_1} {s t : multiset α} (d : (s + t).nodup) :
s.disjoint t

source
theorem multiset.nodup_add_of_nodup {α : Type u_1} {s t : multiset α} (d₁ : s.nodup) (d₂ : t.nodup) :
(s + t).nodup ↔ s.disjoint t

source
theorem multiset.nodup_of_nodup_map {α : Type u_1} {β : Type u_2} (f : α → β) {s : multiset α} (a : (multiset.map f s).nodup) :
s.nodup

source
theorem multiset.nodup_map_on {α : Type u_1} {β : Type u_2} {f : α → β} {s : multiset α} (a : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y → x = y) (a_1 : s.nodup) :
(multiset.map f s).nodup

source
theorem multiset.nodup_map {α : Type u_1} {β : Type u_2} {f : α → β} {s : multiset α} (hf : function.injective f) (a : s.nodup) :
(multiset.map f s).nodup

source
theorem multiset.nodup_filter {α : Type u_1} (p : α → Prop) [decidable_pred p] {s : multiset α} (a : s.nodup) :
(multiset.filter p s).nodup

source
@[simp]
theorem multiset.nodup_attach {α : Type u_1} {s : multiset α} :
s.attach.nodup ↔ s.nodup

source
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) (a : s.nodup) :
(multiset.pmap f s H).nodup

source
@[instance]
def multiset.nodup_decidable {α : Type u_1} [decidable_eq α] (s : multiset α) :
decidable s.nodup

Equations
source
theorem multiset.nodup_erase_eq_filter {α : Type u_1} [decidable_eq α] (a : α) {s : multiset α} (a_1 : s.nodup) :
s.erase a = multiset.filter (λ (_x : α), _x ≠ a) s

source
theorem multiset.nodup_erase_of_nodup {α : Type u_1} [decidable_eq α] (a : α) {l : multiset α} (a_1 : l.nodup) :
(l.erase a).nodup

source
theorem multiset.mem_erase_iff_of_nodup {α : Type u_1} [decidable_eq α] {a b : α} {l : multiset α} (d : l.nodup) :
a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l

source
theorem multiset.mem_erase_of_nodup {α : Type u_1} [decidable_eq α] {a : α} {l : multiset α} (h : l.nodup) :
a ∉ l.erase a

source
theorem multiset.nodup_product {α : Type u_1} {β : Type u_2} {s : multiset α} {t : multiset β} (a : s.nodup) (a_1 : t.nodup) :
(s.product t).nodup

source
theorem multiset.nodup_sigma {α : Type u_1} {σ : α → Type u_2} {s : multiset α} {t : Π (a : α), multiset (σ a)} (a : s.nodup) (a_1 : ∀ (a : α), (t a).nodup) :
(s.sigma t).nodup

source
theorem multiset.nodup_filter_map {α : Type u_1} {β : Type u_2} (f : α → option β) {s : multiset α} (H : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a') (a : s.nodup) :
(multiset.filter_map f s).nodup

source
theorem multiset.nodup_range (n : ℕ) :
(multiset.range n).nodup

source
theorem multiset.nodup_inter_left {α : Type u_1} [decidable_eq α] {s : multiset α} (t : multiset α) (a : s.nodup) :
(s ∩ t).nodup

source
theorem multiset.nodup_inter_right {α : Type u_1} [decidable_eq α] (s : multiset α) {t : multiset α} (a : t.nodup) :
(s ∩ t).nodup

source
@[simp]
theorem multiset.nodup_union {α : Type u_1} [decidable_eq α] {s t : multiset α} :
(s ∪ t).nodup ↔ s.nodup ∧ t.nodup

source
@[simp]
theorem multiset.nodup_powerset {α : Type u_1} {s : multiset α} :
s.powerset.nodup ↔ s.nodup

source
theorem multiset.nodup_powerset_len {α : Type u_1} {n : ℕ} {s : multiset α} (h : s.nodup) :
(multiset.powerset_len n s).nodup

source
@[simp]
theorem multiset.nodup_bind {α : Type u_1} {β : Type u_2} {s : multiset α} {t : α → multiset β} :
(s.bind t).nodup ↔ (∀ (a : α), a ∈ s → (t a).nodup) ∧ multiset.pairwise (λ (a b : α), (t a).disjoint (t b)) s

source
theorem multiset.nodup_ext {α : Type u_1} {s t : multiset α} (a : s.nodup) (a_1 : t.nodup) :
s = t ↔ ∀ (a : α), a ∈ s ↔ a ∈ t

source
theorem multiset.le_iff_subset {α : Type u_1} {s t : multiset α} (a : s.nodup) :
s ≤ t ↔ s ⊆ t

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

source
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

source
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)) :
multiset.map f s = multiset.map g t