The Nodup predicate for multisets without duplicate elements.

TODO

Many of the results in this file can be upstreamed to an earlier file.

@[simp]

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

@[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) : 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) : t.Nodup → s.Nodup

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

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} [DecidableEq α] {s : Multiset α} : s.Nodup ↔ ∀ (a : α), count a s ≤ 1

theorem Multiset.nodup_iff_count_eq_one {α : Type u_1} {s : Multiset α} [DecidableEq α] : s.Nodup ↔ ∀ a ∈ s, count a s = 1

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Multiset.inj_on_of_nodup_map {α : Type u_1} {β : Type u_2} {f : α → β} {s : Multiset α} : (map f s).Nodup → ∀ x ∈ s, ∀ 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) : (map f s).Nodup ↔ ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y

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

@[simp]

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

theorem Multiset.Nodup.attach {α : Type u_1} {s : Multiset α} : s.Nodup → s.attach.Nodup

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 : ∀ a ∈ s, p a} (hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b) : s.Nodup → (Multiset.pmap f s H).Nodup

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

Equations

• s.nodupDecidable = Quotient.recOnSubsingleton s fun (l : List α) => l.nodupDecidable

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

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

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

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

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

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

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

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

@[simp]

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

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

theorem Multiset.mem_sub_of_nodup {α : Type u_1} [DecidableEq α] {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) (i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) (i_surj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), i a ha = b) (h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)) : map f s = map g t