Counting multiplicity in a multiset

countP

def Multiset.countP {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) : ℕ

countP p s counts the number of elements of s (with multiplicity) that satisfy p.

@[simp]

theorem Multiset.coe_countP {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : List α) : countP p ↑l = List.countP (fun (b : α) => decide (p b)) l

@[simp]

theorem Multiset.countP_zero {α : Type u_1} (p : α → Prop) [DecidablePred p] : countP p 0 = 0

@[simp]

theorem Multiset.countP_cons_of_pos {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} (s : Multiset α) : p a → countP p (a ::ₘ s) = countP p s + 1

@[simp]

theorem Multiset.countP_cons_of_neg {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} (s : Multiset α) : ¬p a → countP p (a ::ₘ s) = countP p s

theorem Multiset.countP_cons {α : Type u_1} (p : α → Prop) [DecidablePred p] (b : α) (s : Multiset α) : countP p (b ::ₘ s) = countP p s + if p b then 1 else 0

theorem Multiset.countP_le_card {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) : countP p s ≤ s.card

theorem Multiset.card_eq_countP_add_countP {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) : s.card = countP p s + countP (fun (x : α) => ¬p x) s

theorem Multiset.countP_le_of_le {α : Type u_1} (p : α → Prop) [DecidablePred p] {s t : Multiset α} (h : s ≤ t) : countP p s ≤ countP p t

@[simp]

theorem Multiset.countP_True {α : Type u_1} {s : Multiset α} : countP (fun (x : α) => True) s = s.card

@[simp]

theorem Multiset.countP_False {α : Type u_1} {s : Multiset α} : countP (fun (x : α) => False) s = 0

theorem Multiset.countP_attach {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) : countP (fun (a : { a : α // a ∈ s }) => p ↑a) s.attach = countP p s

theorem Multiset.countP_pos {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Multiset α} : 0 < countP p s ↔ ∃ a ∈ s, p a

theorem Multiset.countP_eq_zero {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Multiset α} : countP p s = 0 ↔ ∀ a ∈ s, ¬p a

theorem Multiset.countP_eq_card {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Multiset α} : countP p s = s.card ↔ ∀ a ∈ s, p a

theorem Multiset.countP_pos_of_mem {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Multiset α} {a : α} (h : a ∈ s) (pa : p a) : 0 < countP p s

theorem Multiset.countP_congr {α : Type u_1} {s s' : Multiset α} (hs : s = s') {p p' : α → Prop} [DecidablePred p] [DecidablePred p'] (hp : ∀ x ∈ s, p x = p' x) : countP p s = countP p' s'

Multiplicity of an element

def Multiset.count {α : Type u_1} [DecidableEq α] (a : α) : Multiset α → ℕ

count a s is the multiplicity of a in s.

@[simp]

theorem Multiset.coe_count {α : Type u_1} [DecidableEq α] (a : α) (l : List α) : count a ↑l = List.count a l

@[simp]

theorem Multiset.count_zero {α : Type u_1} [DecidableEq α] (a : α) : count a 0 = 0

@[simp]

theorem Multiset.count_cons_self {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) : count a (a ::ₘ s) = count a s + 1

@[simp]

theorem Multiset.count_cons_of_ne {α : Type u_1} [DecidableEq α] {a b : α} (h : a ≠ b) (s : Multiset α) : count a (b ::ₘ s) = count a s

theorem Multiset.count_le_card {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) : count a s ≤ s.card

theorem Multiset.count_le_of_le {α : Type u_1} [DecidableEq α] (a : α) {s t : Multiset α} : s ≤ t → count a s ≤ count a t

theorem Multiset.count_le_count_cons {α : Type u_1} [DecidableEq α] (a b : α) (s : Multiset α) : count a s ≤ count a (b ::ₘ s)

theorem Multiset.count_cons {α : Type u_1} [DecidableEq α] (a b : α) (s : Multiset α) : count a (b ::ₘ s) = count a s + if a = b then 1 else 0

theorem Multiset.count_singleton_self {α : Type u_1} [DecidableEq α] (a : α) : count a {a} = 1

theorem Multiset.count_singleton {α : Type u_1} [DecidableEq α] (a b : α) : count a {b} = if a = b then 1 else 0

@[simp]

theorem Multiset.count_attach {α : Type u_1} [DecidableEq α] {s : Multiset α} (a : { x : α // x ∈ s }) : count a s.attach = count (↑a) s

theorem Multiset.count_pos {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : 0 < count a s ↔ a ∈ s

theorem Multiset.one_le_count_iff_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : 1 ≤ count a s ↔ a ∈ s

@[simp]

theorem Multiset.count_eq_zero_of_notMem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} (h : a ∉ s) : count a s = 0

theorem Multiset.count_ne_zero {α : Type u_1} [DecidableEq α] {s : Multiset α} {a : α} : count a s ≠ 0 ↔ a ∈ s

@[simp]

theorem Multiset.count_eq_zero {α : Type u_1} [DecidableEq α] {s : Multiset α} {a : α} : count a s = 0 ↔ a ∉ s

theorem Multiset.count_eq_card {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : count a s = s.card ↔ ∀ x ∈ s, a = x

theorem Multiset.ext {α : Type u_1} [DecidableEq α] {s t : Multiset α} : s = t ↔ ∀ (a : α), count a s = count a t

theorem Multiset.ext' {α : Type u_1} [DecidableEq α] {s t : Multiset α} : (∀ (a : α), count a s = count a t) → s = t

theorem Multiset.ext'_iff {α : Type u_1} [DecidableEq α] {s t : Multiset α} : s = t ↔ ∀ (a : α), count a s = count a t

theorem Multiset.count_injective {α : Type u_1} [DecidableEq α] : Function.Injective fun (s : Multiset α) (a : α) => count a s

theorem Multiset.le_iff_count {α : Type u_1} [DecidableEq α] {s t : Multiset α} : s ≤ t ↔ ∀ (a : α), count a s ≤ count a t

Lift a relation to Multisets

theorem Multiset.Rel.countP_eq {α : Type u_1} (r : α → α → Prop) [IsTrans α r] [Std.Symm r] {s t : Multiset α} (x : α) [DecidablePred (r x)] (h : Rel r s t) : countP (r x) s = countP (r x) 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