Documentation

Init.Data.List.Count

Lemmas about List.countP and List.count. #

countP #

@[simp]
theorem List.countP_nil {α : Type u_1} (p : αBool) :
List.countP p [] = 0
theorem List.countP_go_eq_add {α : Type u_1} (p : αBool) {n : Nat} (l : List α) :
@[simp]
theorem List.countP_cons_of_pos {α : Type u_1} (p : αBool) {a : α} (l : List α) (pa : p a = true) :
List.countP p (a :: l) = List.countP p l + 1
@[simp]
theorem List.countP_cons_of_neg {α : Type u_1} (p : αBool) {a : α} (l : List α) (pa : ¬p a = true) :
theorem List.countP_cons {α : Type u_1} (p : αBool) (a : α) (l : List α) :
List.countP p (a :: l) = List.countP p l + if p a = true then 1 else 0
theorem List.length_eq_countP_add_countP {α : Type u_1} (p : αBool) (l : List α) :
l.length = List.countP p l + List.countP (fun (a : α) => decide ¬p a = true) l
theorem List.countP_eq_length_filter {α : Type u_1} (p : αBool) (l : List α) :
List.countP p l = (List.filter p l).length
theorem List.countP_le_length {α : Type u_1} (p : αBool) {l : List α} :
List.countP p l l.length
@[simp]
theorem List.countP_append {α : Type u_1} (p : αBool) (l₁ : List α) (l₂ : List α) :
List.countP p (l₁ ++ l₂) = List.countP p l₁ + List.countP p l₂
theorem List.countP_pos {α : Type u_1} (p : αBool) {l : List α} :
0 < List.countP p l ∃ (a : α), a l p a = true
theorem List.countP_eq_zero {α : Type u_1} (p : αBool) {l : List α} :
List.countP p l = 0 ∀ (a : α), a l¬p a = true
theorem List.countP_eq_length {α : Type u_1} (p : αBool) {l : List α} :
List.countP p l = l.length ∀ (a : α), a lp a = true
theorem List.Sublist.countP_le {α : Type u_1} (p : αBool) {l₁ : List α} {l₂ : List α} (s : l₁.Sublist l₂) :
theorem List.IsPrefix.countP_le {α : Type u_1} (p : αBool) {l₁ : List α} {l₂ : List α} (s : l₁ <+: l₂) :
theorem List.IsSuffix.countP_le {α : Type u_1} (p : αBool) {l₁ : List α} {l₂ : List α} (s : l₁ <:+ l₂) :
theorem List.IsInfix.countP_le {α : Type u_1} (p : αBool) {l₁ : List α} {l₂ : List α} (s : l₁ <:+: l₂) :
theorem List.countP_filter {α : Type u_1} (p : αBool) (q : αBool) (l : List α) :
List.countP p (List.filter q l) = List.countP (fun (a : α) => decide (p a = true q a = true)) l
@[simp]
theorem List.countP_true {α : Type u_1} {l : List α} :
List.countP (fun (x : α) => true) l = l.length
@[simp]
theorem List.countP_false {α : Type u_1} {l : List α} :
List.countP (fun (x : α) => false) l = 0
@[simp]
theorem List.countP_map {α : Type u_2} {β : Type u_1} (p : βBool) (f : αβ) (l : List α) :
theorem List.countP_mono_left {α : Type u_1} {p : αBool} {q : αBool} {l : List α} (h : ∀ (x : α), x lp x = trueq x = true) :
theorem List.countP_congr {α : Type u_1} {p : αBool} {q : αBool} {l : List α} (h : ∀ (x : α), x l(p x = true q x = true)) :

count #

@[simp]
theorem List.count_nil {α : Type u_1} [BEq α] (a : α) :
List.count a [] = 0
theorem List.count_cons {α : Type u_1} [BEq α] (a : α) (b : α) (l : List α) :
List.count a (b :: l) = List.count a l + if (b == a) = true then 1 else 0
theorem List.count_tail {α : Type u_1} [BEq α] (l : List α) (a : α) (h : l []) :
List.count a l.tail = List.count a l - if (l.head h == a) = true then 1 else 0
theorem List.count_le_length {α : Type u_1} [BEq α] (a : α) (l : List α) :
List.count a l l.length
theorem List.Sublist.count_le {α : Type u_1} [BEq α] {l₁ : List α} {l₂ : List α} (h : l₁.Sublist l₂) (a : α) :
List.count a l₁ List.count a l₂
theorem List.IsPrefix.count_le {α : Type u_1} [BEq α] {l₁ : List α} {l₂ : List α} (h : l₁ <+: l₂) (a : α) :
List.count a l₁ List.count a l₂
theorem List.IsSuffix.count_le {α : Type u_1} [BEq α] {l₁ : List α} {l₂ : List α} (h : l₁ <:+ l₂) (a : α) :
List.count a l₁ List.count a l₂
theorem List.IsInfix.count_le {α : Type u_1} [BEq α] {l₁ : List α} {l₂ : List α} (h : l₁ <:+: l₂) (a : α) :
List.count a l₁ List.count a l₂
theorem List.count_le_count_cons {α : Type u_1} [BEq α] (a : α) (b : α) (l : List α) :
theorem List.count_singleton {α : Type u_1} [BEq α] (a : α) (b : α) :
List.count a [b] = if (b == a) = true then 1 else 0
@[simp]
theorem List.count_append {α : Type u_1} [BEq α] (a : α) (l₁ : List α) (l₂ : List α) :
List.count a (l₁ ++ l₂) = List.count a l₁ + List.count a l₂
@[simp]
theorem List.count_cons_self {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) :
List.count a (a :: l) = List.count a l + 1
@[simp]
theorem List.count_cons_of_ne {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {b : α} (h : a b) (l : List α) :
theorem List.count_singleton_self {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) :
List.count a [a] = 1
theorem List.count_concat_self {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) :
List.count a (l.concat a) = List.count a l + 1
@[simp]
theorem List.count_pos_iff_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} :
0 < List.count a l a l
theorem List.count_eq_zero_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : ¬a l) :
theorem List.not_mem_of_count_eq_zero {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : List.count a l = 0) :
¬a l
theorem List.count_eq_zero {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} :
List.count a l = 0 ¬a l
theorem List.count_eq_length {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} :
List.count a l = l.length ∀ (b : α), b la = b
@[simp]
theorem List.count_replicate_self {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (n : Nat) :
theorem List.count_replicate {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (b : α) (n : Nat) :
List.count a (List.replicate n b) = if (b == a) = true then n else 0
theorem List.filter_beq {α : Type u_1} [BEq α] [LawfulBEq α] (l : List α) (a : α) :
List.filter (fun (x : α) => x == a) l = List.replicate (List.count a l) a
theorem List.filter_eq {α : Type u_1} [DecidableEq α] (l : List α) (a : α) :
List.filter (fun (x : α) => decide (x = a)) l = List.replicate (List.count a l) a
theorem List.le_count_iff_replicate_sublist {α : Type u_1} [BEq α] [LawfulBEq α] {n : Nat} {a : α} {l : List α} :
n List.count a l (List.replicate n a).Sublist l
theorem List.replicate_count_eq_of_count_eq_length {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : List.count a l = l.length) :
@[simp]
theorem List.count_filter {α : Type u_1} [BEq α] [LawfulBEq α] {p : αBool} {a : α} {l : List α} (h : p a = true) :
theorem List.count_le_count_map {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} [DecidableEq β] (l : List α) (f : αβ) (x : α) :
theorem List.count_erase {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (b : α) (l : List α) :
List.count a (l.erase b) = List.count a l - if (b == a) = true then 1 else 0
@[simp]
theorem List.count_erase_self {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) :
List.count a (l.erase a) = List.count a l - 1
@[simp]
theorem List.count_erase_of_ne {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {b : α} (ab : a b) (l : List α) :
List.count a (l.erase b) = List.count a l