Lemmas about List.countP and List.count. #
countP #
theorem
List.countP_go_eq_add
{α : Type u_1}
(p : α → Bool)
{n : Nat}
(l : List α)
:
List.countP.go p l n = n + List.countP.go p l 0
@[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)
:
List.countP p (a :: l) = List.countP p l
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.Sublist.countP_le
{α : Type u_1}
(p : α → Bool)
{l₁ : List α}
{l₂ : List α}
(s : l₁.Sublist l₂)
:
List.countP p l₁ ≤ List.countP p 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]
@[simp]
theorem
List.countP_map
{α : Type u_2}
{β : Type u_1}
(p : β → Bool)
(f : α → β)
(l : List α)
:
List.countP p (List.map f l) = List.countP (p ∘ f) l
theorem
List.countP_mono_left
{α : Type u_1}
{p : α → Bool}
{q : α → Bool}
{l : List α}
(h : ∀ (x : α), x ∈ l → p x = true → q x = true)
:
List.countP p l ≤ List.countP q l
theorem
List.countP_congr
{α : Type u_1}
{p : α → Bool}
{q : α → Bool}
{l : List α}
(h : ∀ (x : α), x ∈ l → (p x = true ↔ q x = true))
:
List.countP p l = List.countP q l
count #
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.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.count_le_count_cons
{α : Type u_1}
[BEq α]
(a : α)
(b : α)
(l : List α)
:
List.count a l ≤ List.count a (b :: l)
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 α)
:
List.count a (b :: l) = List.count a l
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)
:
List.count a l = 0
theorem
List.not_mem_of_count_eq_zero
{α : Type u_1}
[BEq α]
[LawfulBEq α]
{a : α}
{l : List α}
(h : List.count a l = 0)
:
@[simp]
theorem
List.count_replicate_self
{α : Type u_1}
[BEq α]
[LawfulBEq α]
(a : α)
(n : Nat)
:
List.count a (List.replicate n a) = n
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)
:
List.replicate (List.count a l) a = l
@[simp]
theorem
List.count_filter
{α : Type u_1}
[BEq α]
[LawfulBEq α]
{p : α → Bool}
{a : α}
{l : List α}
(h : p a = true)
:
List.count a (List.filter p l) = List.count a l
theorem
List.count_le_count_map
{α : Type u_2}
[BEq α]
[LawfulBEq α]
{β : Type u_1}
[DecidableEq β]
(l : List α)
(f : α → β)
(x : α)
:
List.count x l ≤ List.count (f x) (List.map f l)
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