Documentation

Init.Data.Array.Count

Lemmas about Array.countP and Array.count. #

countP #

source
@[simp]
theorem List.countP_toArray {α : Type u_1} {p : α → Bool} {l : List α} :
Array.countP p l.toArray = countP p l
source
@[simp]
theorem Array.countP_toList {α : Type u_1} {p : α → Bool} {xs : Array α} :
List.countP p xs.toList = countP p xs
source
@[simp]
theorem Array.countP_empty {α : Type u_1} {p : α → Bool} :
countP p #[] = 0
source
@[simp]
theorem Array.countP_push_of_pos {α : Type u_1} {p : α → Bool} {a : α} {xs : Array α} (pa : p a = true) :
countP p (xs.push a) = countP p xs + 1
source
@[simp]
theorem Array.countP_push_of_neg {α : Type u_1} {p : α → Bool} {a : α} {xs : Array α} (pa : ¬p a = true) :
countP p (xs.push a) = countP p xs
source
theorem Array.countP_push {α : Type u_1} {p : α → Bool} {a : α} {xs : Array α} :
countP p (xs.push a) = countP p xs + if p a = true then 1 else 0
source
@[simp]
theorem Array.countP_singleton {α : Type u_1} {p : α → Bool} {a : α} :
countP p #[a] = if p a = true then 1 else 0
source
theorem Array.size_eq_countP_add_countP {α : Type u_1} {p : α → Bool} {xs : Array α} :
xs.size = countP p xs + countP (fun (a : α) => decide ¬p a = true) xs
source
theorem Array.countP_eq_size_filter {α : Type u_1} {p : α → Bool} {xs : Array α} :
countP p xs = (filter p xs).size
source
theorem Array.countP_eq_size_filter' {α : Type u_1} {p : α → Bool} :
countP p = size ∘ fun (as : Array α) => filter p as
source
theorem Array.countP_le_size {α : Type u_1} {p : α → Bool} {xs : Array α} :
countP p xs ≤ xs.size
source
@[simp]
theorem Array.countP_append {α : Type u_1} {p : α → Bool} {xs ys : Array α} :
countP p (xs ++ ys) = countP p xs + countP p ys
source
@[simp]
theorem Array.countP_pos_iff {α✝ : Type u_1} {xs : Array α✝} {p : α✝ → Bool} :
0 < countP p xs ↔ ∃ (a : α✝), a ∈ xs ∧ p a = true
source
@[simp]
theorem Array.one_le_countP_iff {α✝ : Type u_1} {xs : Array α✝} {p : α✝ → Bool} :
1 ≤ countP p xs ↔ ∃ (a : α✝), a ∈ xs ∧ p a = true
source
@[simp]
theorem Array.countP_eq_zero {α✝ : Type u_1} {xs : Array α✝} {p : α✝ → Bool} :
countP p xs = 0 ↔ ∀ (a : α✝), a ∈ xs → ¬p a = true
source
@[simp]
theorem Array.countP_eq_size {α✝ : Type u_1} {xs : Array α✝} {p : α✝ → Bool} :
countP p xs = xs.size ↔ ∀ (a : α✝), a ∈ xs → p a = true
source
theorem Array.countP_replicate {α : Type u_1} {p : α → Bool} {a : α} {n : Nat} :
countP p (replicate n a) = if p a = true then n else 0
source
@[reducible, inline, deprecated Array.countP_replicate (since := "2025-03-18")]
abbrev Array.countP_mkArray {α : Type u_1} {p : α → Bool} {a : α} {n : Nat} :
countP p (replicate n a) = if p a = true then n else 0
Equations
source
theorem Array.boole_getElem_le_countP {α : Type u_1} {p : α → Bool} {xs : Array α} {i : Nat} (h : i < xs.size) :
(if p xs[i] = true then 1 else 0) ≤ countP p xs
source
theorem Array.countP_set {α : Type u_1} {p : α → Bool} {xs : Array α} {i : Nat} {a : α} (h : i < xs.size) :
countP p (xs.set i a h) = (countP p xs - if p xs[i] = true then 1 else 0) + if p a = true then 1 else 0
source
theorem Array.countP_filter {α : Type u_1} {p q : α → Bool} {xs : Array α} :
countP p (filter q xs) = countP (fun (a : α) => p a && q a) xs
source
@[simp]
theorem Array.countP_true {α : Type u_1} :
(countP fun (x : α) => true) = size
source
@[simp]
theorem Array.countP_false {α : Type u_1} :
(countP fun (x : α) => false) = Function.const (Array α) 0
source
@[simp]
theorem Array.countP_map {α : Type u_2} {β : Type u_1} {p : β → Bool} {f : α → β} {xs : Array α} :
countP p (map f xs) = countP (p ∘ f) xs
source
theorem Array.size_filterMap_eq_countP {α : Type u_2} {β : Type u_1} {f : α → Option β} {xs : Array α} :
(filterMap f xs).size = countP (fun (a : α) => (f a).isSome) xs
source
theorem Array.countP_filterMap {α : Type u_2} {β : Type u_1} {p : β → Bool} {f : α → Option β} {xs : Array α} :
countP p (filterMap f xs) = countP (fun (a : α) => (Option.map p (f a)).getD false) xs
source
@[simp]
theorem Array.countP_flatten {α : Type u_1} {p : α → Bool} {xss : Array (Array α)} :
countP p xss.flatten = (map (countP p) xss).sum
source
theorem Array.countP_flatMap {α : Type u_2} {β : Type u_1} {p : β → Bool} {xs : Array α} {f : α → Array β} :
countP p (flatMap f xs) = (map (countP p ∘ f) xs).sum
source
@[simp]
theorem Array.countP_reverse {α : Type u_1} {p : α → Bool} {xs : Array α} :
countP p xs.reverse = countP p xs
source
theorem Array.countP_mono_left {α : Type u_1} {p q : α → Bool} {xs : Array α} (h : ∀ (x : α), x ∈ xs → p x = true → q x = true) :
countP p xs ≤ countP q xs
source
theorem Array.countP_congr {α : Type u_1} {p q : α → Bool} {xs : Array α} (h : ∀ (x : α), x ∈ xs → (p x = true ↔ q x = true)) :
countP p xs = countP q xs

count #

source
@[simp]
theorem List.count_toArray {α : Type u_1} [BEq α] {l : List α} {a : α} :
Array.count a l.toArray = count a l
source
@[simp]
theorem Array.count_toList {α : Type u_1} [BEq α] {xs : Array α} {a : α} :
List.count a xs.toList = count a xs
source
@[simp]
theorem Array.count_empty {α : Type u_1} [BEq α] {a : α} :
count a #[] = 0
source
theorem Array.count_push {α : Type u_1} [BEq α] {a b : α} {xs : Array α} :
count a (xs.push b) = count a xs + if (b == a) = true then 1 else 0
source
theorem Array.count_eq_countP {α : Type u_1} [BEq α] {a : α} {xs : Array α} :
count a xs = countP (fun (x : α) => x == a) xs
source
theorem Array.count_eq_countP' {α : Type u_1} [BEq α] {a : α} :
count a = countP fun (x : α) => x == a
source
theorem Array.count_le_size {α : Type u_1} [BEq α] {a : α} {xs : Array α} :
count a xs ≤ xs.size
source
theorem Array.count_le_count_push {α : Type u_1} [BEq α] {a b : α} {xs : Array α} :
count a xs ≤ count a (xs.push b)
source
theorem Array.count_singleton {α : Type u_1} [BEq α] {a b : α} :
count a #[b] = if (b == a) = true then 1 else 0
source
@[simp]
theorem Array.count_append {α : Type u_1} [BEq α] {a : α} {xs ys : Array α} :
count a (xs ++ ys) = count a xs + count a ys
source
@[simp]
theorem Array.count_flatten {α : Type u_1} [BEq α] {a : α} {xss : Array (Array α)} :
count a xss.flatten = (map (count a) xss).sum
source
@[simp]
theorem Array.count_reverse {α : Type u_1} [BEq α] {a : α} {xs : Array α} :
count a xs.reverse = count a xs
source
theorem Array.boole_getElem_le_count {α : Type u_1} [BEq α] {xs : Array α} {i : Nat} {a : α} (h : i < xs.size) :
(if (xs[i] == a) = true then 1 else 0) ≤ count a xs
source
theorem Array.count_set {α : Type u_1} [BEq α] {xs : Array α} {i : Nat} {a b : α} (h : i < xs.size) :
count b (xs.set i a h) = (count b xs - if (xs[i] == b) = true then 1 else 0) + if (a == b) = true then 1 else 0
source
@[simp]
theorem Array.count_push_self {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
count a (xs.push a) = count a xs + 1
source
@[simp]
theorem Array.count_push_of_ne {α : Type u_1} [BEq α] [LawfulBEq α] {b a : α} {xs : Array α} (h : b ≠ a) :
count a (xs.push b) = count a xs
source
theorem Array.count_singleton_self {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} :
count a #[a] = 1
source
@[simp]
theorem Array.count_pos_iff {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
0 < count a xs ↔ a ∈ xs
source
@[simp]
theorem Array.one_le_count_iff {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
1 ≤ count a xs ↔ a ∈ xs
source
theorem Array.count_eq_zero_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {xs : Array α} (h : ¬a ∈ xs) :
count a xs = 0
source
theorem Array.not_mem_of_count_eq_zero {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {xs : Array α} (h : count a xs = 0) :
¬a ∈ xs
source
theorem Array.count_eq_zero {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
count a xs = 0 ↔ ¬a ∈ xs
source
theorem Array.count_eq_size {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
count a xs = xs.size ↔ ∀ (b : α), b ∈ xs → a = b
source
@[simp]
theorem Array.count_replicate_self {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {n : Nat} :
count a (replicate n a) = n
source
@[reducible, inline, deprecated Array.count_replicate_self (since := "2025-03-18")]
abbrev Array.count_mkArray_self {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {n : Nat} :
count a (replicate n a) = n
Equations
source
theorem Array.count_replicate {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} {n : Nat} :
count a (replicate n b) = if (b == a) = true then n else 0
source
@[reducible, inline, deprecated Array.count_replicate (since := "2025-03-18")]
abbrev Array.count_mkArray {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} {n : Nat} :
count a (replicate n b) = if (b == a) = true then n else 0
Equations
source
theorem Array.filter_beq {α : Type u_1} [BEq α] [LawfulBEq α] {xs : Array α} (a : α) :
filter (fun (x : α) => x == a) xs = replicate (count a xs) a
source
theorem Array.filter_eq {α : Type u_1} [DecidableEq α] {xs : Array α} (a : α) :
filter (fun (x : α) => decide (x = a)) xs = replicate (count a xs) a
source
theorem Array.replicate_count_eq_of_count_eq_size {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {xs : Array α} (h : count a xs = xs.size) :
replicate (count a xs) a = xs
source
@[reducible, inline, deprecated Array.replicate_count_eq_of_count_eq_size (since := "2025-03-18")]
abbrev Array.mkArray_count_eq_of_count_eq_size {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {xs : Array α} (h : count a xs = xs.size) :
replicate (count a xs) a = xs
Equations
source
@[simp]
theorem Array.count_filter {α : Type u_1} [BEq α] [LawfulBEq α] {p : α → Bool} {a : α} {xs : Array α} (h : p a = true) :
count a (filter p xs) = count a xs
source
theorem Array.count_le_count_map {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} [DecidableEq β] {xs : Array α} {f : α → β} {x : α} :
count x xs ≤ count (f x) (map f xs)
source
theorem Array.count_filterMap {β : Type u_1} {α : Type u_2} [BEq β] {b : β} {f : α → Option β} {xs : Array α} :
count b (filterMap f xs) = countP (fun (a : α) => f a == some b) xs
source
theorem Array.count_flatMap {β : Type u_1} {α : Type u_2} [BEq β] {xs : Array α} {f : α → Array β} {x : β} :
count x (flatMap f xs) = (map (count x ∘ f) xs).sum