The nodup predicate for multisets without duplicate elements.
nodup s means that s has no duplicates, i.e. the multiplicity of
any element is at most 1.
Equations
- s.nodup = quot.lift_on s list.nodup multiset.nodup._proof_1
theorem
multiset.nodup_iff_count_le_one
{α : Type u_1}
[decidable_eq α]
{s : multiset α} :
s.nodup ↔ ∀ (a : α), multiset.count a s ≤ 1
@[simp]
theorem
multiset.count_eq_one_of_mem
{α : Type u_1}
[decidable_eq α]
{a : α}
{s : multiset α} :
s.nodup → a ∈ s → multiset.count a s = 1
theorem
multiset.nodup_iff_pairwise
{α : Type u_1}
{s : multiset α} :
s.nodup ↔ multiset.pairwise ne s
theorem
multiset.pairwise_of_nodup
{α : Type u_1}
{r : α → α → Prop}
{s : multiset α} :
(∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ≠ b → r a b) → s.nodup → multiset.pairwise r s
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 : α) :
theorem
multiset.nodup_of_nodup_map
{α : Type u_1}
{β : Type u_2}
(f : α → β)
{s : multiset α} :
(multiset.map f s).nodup → s.nodup
theorem
multiset.nodup_map
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{s : multiset α} :
function.injective f → s.nodup → (multiset.map f s).nodup
theorem
multiset.nodup_filter
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
{s : multiset α} :
s.nodup → (multiset.filter p s).nodup
theorem
multiset.nodup_pmap
{α : Type u_1}
{β : Type u_2}
{p : α → Prop}
{f : Π (a : α), p a → β}
{s : multiset α}
{H : ∀ (a : α), a ∈ s → p a} :
(∀ (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]
Equations
- s.nodup_decidable = quotient.rec_on_subsingleton s (λ (l : list α), l.nodup_decidable)
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_filter_map
{α : Type u_1}
{β : Type u_2}
(f : α → option β)
{s : multiset α} :
theorem
multiset.nodup_inter_left
{α : Type u_1}
[decidable_eq α]
{s : multiset α}
(t : multiset α) :
theorem
multiset.nodup_inter_right
{α : Type u_1}
[decidable_eq α]
(s : multiset α)
{t : multiset α} :
@[simp]
theorem
multiset.nodup_powerset_len
{α : Type u_1}
{n : ℕ}
{s : multiset α} :
s.nodup → (multiset.powerset_len n s).nodup