Lemmas about Array.countP and Array.count.

countP

@[simp]

theorem Array.countP_empty {α : Type u_1} (p : α → Bool) : countP p #[] = 0

@[simp]

theorem Array.countP_push_of_pos {α : Type u_1} (p : α → Bool) {a : α} (l : Array α) (pa : p a = true) : countP p (l.push a) = countP p l + 1

@[simp]

theorem Array.countP_push_of_neg {α : Type u_1} (p : α → Bool) {a : α} (l : Array α) (pa : ¬p a = true) : countP p (l.push a) = countP p l

theorem Array.countP_push {α : Type u_1} (p : α → Bool) (a : α) (l : Array α) : countP p (l.push a) = countP p l + if p a = true then 1 else 0

@[simp]

theorem Array.countP_singleton {α : Type u_1} (p : α → Bool) (a : α) : countP p #[a] = if p a = true then 1 else 0

theorem Array.size_eq_countP_add_countP {α : Type u_1} (p : α → Bool) (l : Array α) : l.size = countP p l + countP (fun (a : α) => decide ¬p a = true) l

theorem Array.countP_eq_size_filter {α : Type u_1} (p : α → Bool) (l : Array α) : countP p l = (filter p l).size

theorem Array.countP_eq_size_filter' {α : Type u_1} (p : α → Bool) : countP p = size ∘ fun (as : Array α) => filter p as

theorem Array.countP_le_size {α : Type u_1} (p : α → Bool) {l : Array α} : countP p l ≤ l.size

@[simp]

theorem Array.countP_append {α : Type u_1} (p : α → Bool) (l₁ l₂ : Array α) : countP p (l₁ ++ l₂) = countP p l₁ + countP p l₂

@[simp]

theorem Array.countP_pos_iff {α✝ : Type u_1} {l : Array α✝} {p : α✝ → Bool} : 0 < countP p l ↔ ∃ (a : α✝), a ∈ l ∧ p a = true

@[simp]

theorem Array.one_le_countP_iff {α✝ : Type u_1} {l : Array α✝} {p : α✝ → Bool} : 1 ≤ countP p l ↔ ∃ (a : α✝), a ∈ l ∧ p a = true

@[simp]

theorem Array.countP_eq_zero {α✝ : Type u_1} {l : Array α✝} {p : α✝ → Bool} : countP p l = 0 ↔ ∀ (a : α✝), a ∈ l → ¬p a = true

@[simp]

theorem Array.countP_eq_size {α✝ : Type u_1} {l : Array α✝} {p : α✝ → Bool} : countP p l = l.size ↔ ∀ (a : α✝), a ∈ l → p a = true

theorem Array.countP_mkArray {α : Type u_1} (p : α → Bool) (a : α) (n : Nat) : countP p (mkArray n a) = if p a = true then n else 0

theorem Array.boole_getElem_le_countP {α : Type u_1} (p : α → Bool) (l : Array α) (i : Nat) (h : i < l.size) : (if p l[i] = true then 1 else 0) ≤ countP p l

theorem Array.countP_set {α : Type u_1} (p : α → Bool) (l : Array α) (i : Nat) (a : α) (h : i < l.size) : countP p (l.set i a h) = (countP p l - if p l[i] = true then 1 else 0) + if p a = true then 1 else 0

theorem Array.countP_filter {α : Type u_1} (p q : α → Bool) (l : Array α) : countP p (filter q l) = countP (fun (a : α) => p a && q a) l

@[simp]

theorem Array.countP_true {α : Type u_1} : (countP fun (x : α) => true) = size

@[simp]

theorem Array.countP_false {α : Type u_1} : (countP fun (x : α) => false) = Function.const (Array α) 0

@[simp]

theorem Array.countP_map {α : Type u_2} {β : Type u_1} (p : β → Bool) (f : α → β) (l : Array α) : countP p (map f l) = countP (p ∘ f) l

theorem Array.size_filterMap_eq_countP {α : Type u_2} {β : Type u_1} (f : α → Option β) (l : Array α) : (filterMap f l).size = countP (fun (a : α) => (f a).isSome) l

theorem Array.countP_filterMap {α : Type u_2} {β : Type u_1} (p : β → Bool) (f : α → Option β) (l : Array α) : countP p (filterMap f l) = countP (fun (a : α) => (Option.map p (f a)).getD false) l

@[simp]

theorem Array.countP_flatten {α : Type u_1} (p : α → Bool) (l : Array (Array α)) : countP p l.flatten = (map (countP p) l).sum

theorem Array.countP_flatMap {α : Type u_2} {β : Type u_1} (p : β → Bool) (l : Array α) (f : α → Array β) : countP p (flatMap f l) = (map (countP p ∘ f) l).sum

@[simp]

theorem Array.countP_reverse {α : Type u_1} (p : α → Bool) (l : Array α) : countP p l.reverse = countP p l

theorem Array.countP_mono_left {α : Type u_1} {p q : α → Bool} {l : Array α} (h : ∀ (x : α), x ∈ l → p x = true → q x = true) : countP p l ≤ countP q l

theorem Array.countP_congr {α : Type u_1} {p q : α → Bool} {l : Array α} (h : ∀ (x : α), x ∈ l → (p x = true ↔ q x = true)) : countP p l = countP q l

count

@[simp]

theorem Array.count_empty {α : Type u_1} [BEq α] (a : α) : count a #[] = 0

theorem Array.count_push {α : Type u_1} [BEq α] (a b : α) (l : Array α) : count a (l.push b) = count a l + if (b == a) = true then 1 else 0

theorem Array.count_eq_countP {α : Type u_1} [BEq α] (a : α) (l : Array α) : count a l = countP (fun (x : α) => x == a) l

theorem Array.count_eq_countP' {α : Type u_1} [BEq α] {a : α} : count a = countP fun (x : α) => x == a

theorem Array.count_le_size {α : Type u_1} [BEq α] (a : α) (l : Array α) : count a l ≤ l.size

theorem Array.count_le_count_push {α : Type u_1} [BEq α] (a b : α) (l : Array α) : count a l ≤ count a (l.push b)

@[simp]

theorem Array.count_singleton {α : Type u_1} [BEq α] (a b : α) : count a #[b] = if (b == a) = true then 1 else 0

@[simp]

theorem Array.count_append {α : Type u_1} [BEq α] (a : α) (l₁ l₂ : Array α) : count a (l₁ ++ l₂) = count a l₁ + count a l₂

@[simp]

theorem Array.count_flatten {α : Type u_1} [BEq α] (a : α) (l : Array (Array α)) : count a l.flatten = (map (count a) l).sum

@[simp]

theorem Array.count_reverse {α : Type u_1} [BEq α] (a : α) (l : Array α) : count a l.reverse = count a l

theorem Array.boole_getElem_le_count {α : Type u_1} [BEq α] (a : α) (l : Array α) (i : Nat) (h : i < l.size) : (if (l[i] == a) = true then 1 else 0) ≤ count a l

theorem Array.count_set {α : Type u_1} [BEq α] (a b : α) (l : Array α) (i : Nat) (h : i < l.size) : count b (l.set i a h) = (count b l - if (l[i] == b) = true then 1 else 0) + if (a == b) = true then 1 else 0

@[simp]

theorem Array.count_push_self {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : Array α) : count a (l.push a) = count a l + 1

@[simp]

theorem Array.count_push_of_ne {α : Type u_1} [BEq α] [LawfulBEq α] {b a : α} (h : b ≠ a) (l : Array α) : count a (l.push b) = count a l

theorem Array.count_singleton_self {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) : count a #[a] = 1

@[simp]

theorem Array.count_pos_iff {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : Array α} : 0 < count a l ↔ a ∈ l

@[simp]

theorem Array.one_le_count_iff {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : Array α} : 1 ≤ count a l ↔ a ∈ l

theorem Array.count_eq_zero_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : Array α} (h : ¬a ∈ l) : count a l = 0

theorem Array.not_mem_of_count_eq_zero {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : Array α} (h : count a l = 0) : ¬a ∈ l

theorem Array.count_eq_zero {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : Array α} : count a l = 0 ↔ ¬a ∈ l

theorem Array.count_eq_size {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : Array α} : count a l = l.size ↔ ∀ (b : α), b ∈ l → a = b

@[simp]

theorem Array.count_mkArray_self {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (n : Nat) : count a (mkArray n a) = n

theorem Array.count_mkArray {α : Type u_1} [BEq α] [LawfulBEq α] (a b : α) (n : Nat) : count a (mkArray n b) = if (b == a) = true then n else 0

theorem Array.filter_beq {α : Type u_1} [BEq α] [LawfulBEq α] (l : Array α) (a : α) : filter (fun (x : α) => x == a) l = mkArray (count a l) a

theorem Array.filter_eq {α : Type u_1} [DecidableEq α] (l : Array α) (a : α) : filter (fun (x : α) => decide (x = a)) l = mkArray (count a l) a

theorem Array.mkArray_count_eq_of_count_eq_size {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : Array α} (h : count a l = l.size) : mkArray (count a l) a = l

@[simp]

theorem Array.count_filter {α : Type u_1} [BEq α] [LawfulBEq α] {p : α → Bool} {a : α} {l : Array α} (h : p a = true) : count a (filter p l) = count a l

theorem Array.count_le_count_map {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} [DecidableEq β] (l : Array α) (f : α → β) (x : α) : count x l ≤ count (f x) (map f l)

theorem Array.count_filterMap {β : Type u_1} {α : Type u_2} [BEq β] (b : β) (f : α → Option β) (l : Array α) : count b (filterMap f l) = countP (fun (a : α) => f a == some b) l

theorem Array.count_flatMap {β : Type u_1} {α : Type u_2} [BEq β] (l : Array α) (f : α → Array β) (x : β) : count x (flatMap f l) = (map (count x ∘ f) l).sum