Documentation

Init.Data.List.Count

Lemmas about List.countP and List.count. #

countP #

source
@[simp]
theorem List.countP_nil {α : Type u_1} (p : α → Bool) :
countP p [] = 0
source
theorem List.countP_go_eq_add {α : Type u_1} (p : α → Bool) {n : Nat} (l : List α) :
countP.go p l n = n + countP.go p l 0
source
@[simp]
theorem List.countP_cons_of_pos {α : Type u_1} (p : α → Bool) {a : α} (l : List α) (pa : p a = true) :
countP p (a :: l) = countP p l + 1
source
@[simp]
theorem List.countP_cons_of_neg {α : Type u_1} (p : α → Bool) {a : α} (l : List α) (pa : ¬p a = true) :
countP p (a :: l) = countP p l
source
theorem List.countP_cons {α : Type u_1} (p : α → Bool) (a : α) (l : List α) :
countP p (a :: l) = countP p l + if p a = true then 1 else 0
source
@[simp]
theorem List.countP_singleton {α : Type u_1} (p : α → Bool) (a : α) :
countP p [a] = if p a = true then 1 else 0
source
theorem List.length_eq_countP_add_countP {α : Type u_1} (p : α → Bool) (l : List α) :
l.length = countP p l + countP (fun (a : α) => decide ¬p a = true) l
source
theorem List.countP_eq_length_filter {α : Type u_1} (p : α → Bool) (l : List α) :
countP p l = (filter p l).length
source
theorem List.countP_eq_length_filter' {α : Type u_1} (p : α → Bool) :
countP p = length ∘ filter p
source
theorem List.countP_le_length {α : Type u_1} (p : α → Bool) {l : List α} :
countP p l ≤ l.length
source
@[simp]
theorem List.countP_append {α : Type u_1} (p : α → Bool) (l₁ l₂ : List α) :
countP p (l₁ ++ l₂) = countP p l₁ + countP p l₂
source
@[simp]
theorem List.countP_pos_iff {α✝ : Type u_1} {l : List α✝} {p : α✝ → Bool} :
0 < countP p l ↔ ∃ (a : α✝), a ∈ l ∧ p a = true
source
@[reducible, inline, deprecated List.countP_pos_iff (since := "2024-09-09")]
abbrev List.countP_pos {α✝ : Type u_1} {l : List α✝} {p : α✝ → Bool} :
0 < countP p l ↔ ∃ (a : α✝), a ∈ l ∧ p a = true
Equations
Instances For
    source
    @[simp]
    theorem List.one_le_countP_iff {α✝ : Type u_1} {l : List α✝} {p : α✝ → Bool} :
    1 ≤ countP p l ↔ ∃ (a : α✝), a ∈ l ∧ p a = true
    source
    @[simp]
    theorem List.countP_eq_zero {α✝ : Type u_1} {l : List α✝} {p : α✝ → Bool} :
    countP p l = 0 ↔ ∀ (a : α✝), a ∈ l → ¬p a = true
    source
    @[simp]
    theorem List.countP_eq_length {α✝ : Type u_1} {l : List α✝} {p : α✝ → Bool} :
    countP p l = l.length ↔ ∀ (a : α✝), a ∈ l → p a = true
    source
    theorem List.countP_replicate {α : Type u_1} (p : α → Bool) (a : α) (n : Nat) :
    countP p (replicate n a) = if p a = true then n else 0
    source
    theorem List.boole_getElem_le_countP {α : Type u_1} (p : α → Bool) (l : List α) (i : Nat) (h : i < l.length) :
    (if p l[i] = true then 1 else 0) ≤ countP p l
    source
    theorem List.Sublist.countP_le {α : Type u_1} (p : α → Bool) {l₁ l₂ : List α} (s : l₁.Sublist l₂) :
    countP p l₁ ≤ countP p l₂
    source
    theorem List.IsPrefix.countP_le {α : Type u_1} (p : α → Bool) {l₁ l₂ : List α} (s : l₁ <+: l₂) :
    countP p l₁ ≤ countP p l₂
    source
    theorem List.IsSuffix.countP_le {α : Type u_1} (p : α → Bool) {l₁ l₂ : List α} (s : l₁ <:+ l₂) :
    countP p l₁ ≤ countP p l₂
    source
    theorem List.IsInfix.countP_le {α : Type u_1} (p : α → Bool) {l₁ l₂ : List α} (s : l₁ <:+: l₂) :
    countP p l₁ ≤ countP p l₂
    source
    theorem List.countP_tail_le {α : Type u_1} (p : α → Bool) (l : List α) :
    countP p l.tail ≤ countP p l
    source
    theorem List.countP_filter {α : Type u_1} (p q : α → Bool) (l : List α) :
    countP p (filter q l) = countP (fun (a : α) => p a && q a) l
    source
    @[simp]
    theorem List.countP_true {α : Type u_1} :
    (countP fun (x : α) => true) = length
    source
    @[simp]
    theorem List.countP_false {α : Type u_1} :
    (countP fun (x : α) => false) = Function.const (List α) 0
    source
    @[simp]
    theorem List.countP_map {α : Type u_2} {β : Type u_1} (p : β → Bool) (f : α → β) (l : List α) :
    countP p (map f l) = countP (p ∘ f) l
    source
    theorem List.length_filterMap_eq_countP {α : Type u_2} {β : Type u_1} (f : α → Option β) (l : List α) :
    (filterMap f l).length = countP (fun (a : α) => (f a).isSome) l
    source
    theorem List.countP_filterMap {α : Type u_2} {β : Type u_1} (p : β → Bool) (f : α → Option β) (l : List α) :
    countP p (filterMap f l) = countP (fun (a : α) => (Option.map p (f a)).getD false) l
    source
    @[simp]
    theorem List.countP_flatten {α : Type u_1} (p : α → Bool) (l : List (List α)) :
    countP p l.flatten = (map (countP p) l).sum
    source
    @[reducible, inline, deprecated List.countP_flatten (since := "2024-10-14")]
    abbrev List.countP_join {α : Type u_1} (p : α → Bool) (l : List (List α)) :
    countP p l.flatten = (map (countP p) l).sum
    Equations
    Instances For
      source
      theorem List.countP_flatMap {α : Type u_2} {β : Type u_1} (p : β → Bool) (l : List α) (f : α → List β) :
      countP p (flatMap f l) = (map (countP p ∘ f) l).sum
      source
      @[simp]
      theorem List.countP_reverse {α : Type u_1} (p : α → Bool) (l : List α) :
      countP p l.reverse = countP p l
      source
      theorem List.countP_mono_left {α : Type u_1} {p q : α → Bool} {l : List α} (h : ∀ (x : α), x ∈ l → p x = true → q x = true) :
      countP p l ≤ countP q l
      source
      theorem List.countP_congr {α : Type u_1} {p q : α → Bool} {l : List α} (h : ∀ (x : α), x ∈ l → (p x = true ↔ q x = true)) :
      countP p l = countP q l

      count #

      source
      @[simp]
      theorem List.count_nil {α : Type u_1} [BEq α] (a : α) :
      count a [] = 0
      source
      theorem List.count_cons {α : Type u_1} [BEq α] (a b : α) (l : List α) :
      count a (b :: l) = count a l + if (b == a) = true then 1 else 0
      source
      theorem List.count_eq_countP {α : Type u_1} [BEq α] (a : α) (l : List α) :
      count a l = countP (fun (x : α) => x == a) l
      source
      theorem List.count_eq_countP' {α : Type u_1} [BEq α] {a : α} :
      count a = countP fun (x : α) => x == a
      source
      theorem List.count_tail {α : Type u_1} [BEq α] (l : List α) (a : α) (h : l ≠ []) :
      count a l.tail = count a l - if (l.head h == a) = true then 1 else 0
      source
      theorem List.count_le_length {α : Type u_1} [BEq α] (a : α) (l : List α) :
      count a l ≤ l.length
      source
      theorem List.Sublist.count_le {α : Type u_1} [BEq α] {l₁ l₂ : List α} (h : l₁.Sublist l₂) (a : α) :
      count a l₁ ≤ count a l₂
      source
      theorem List.IsPrefix.count_le {α : Type u_1} [BEq α] {l₁ l₂ : List α} (h : l₁ <+: l₂) (a : α) :
      count a l₁ ≤ count a l₂
      source
      theorem List.IsSuffix.count_le {α : Type u_1} [BEq α] {l₁ l₂ : List α} (h : l₁ <:+ l₂) (a : α) :
      count a l₁ ≤ count a l₂
      source
      theorem List.IsInfix.count_le {α : Type u_1} [BEq α] {l₁ l₂ : List α} (h : l₁ <:+: l₂) (a : α) :
      count a l₁ ≤ count a l₂
      source
      theorem List.count_tail_le {α : Type u_1} [BEq α] (a : α) (l : List α) :
      count a l.tail ≤ count a l
      source
      theorem List.count_le_count_cons {α : Type u_1} [BEq α] (a b : α) (l : List α) :
      count a l ≤ count a (b :: l)
      source
      theorem List.count_singleton {α : Type u_1} [BEq α] (a b : α) :
      count a [b] = if (b == a) = true then 1 else 0
      source
      @[simp]
      theorem List.count_append {α : Type u_1} [BEq α] (a : α) (l₁ l₂ : List α) :
      count a (l₁ ++ l₂) = count a l₁ + count a l₂
      source
      theorem List.count_flatten {α : Type u_1} [BEq α] (a : α) (l : List (List α)) :
      count a l.flatten = (map (count a) l).sum
      source
      @[reducible, inline, deprecated List.count_flatten (since := "2024-10-14")]
      abbrev List.count_join {α : Type u_1} [BEq α] (a : α) (l : List (List α)) :
      count a l.flatten = (map (count a) l).sum
      Equations
      Instances For
        source
        @[simp]
        theorem List.count_reverse {α : Type u_1} [BEq α] (a : α) (l : List α) :
        count a l.reverse = count a l
        source
        theorem List.boole_getElem_le_count {α : Type u_1} [BEq α] (a : α) (l : List α) (i : Nat) (h : i < l.length) :
        (if (l[i] == a) = true then 1 else 0) ≤ count a l
        source
        @[simp]
        theorem List.count_cons_self {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) :
        count a (a :: l) = count a l + 1
        source
        @[simp]
        theorem List.count_cons_of_ne {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} (h : a ≠ b) (l : List α) :
        count a (b :: l) = count a l
        source
        theorem List.count_singleton_self {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) :
        count a [a] = 1
        source
        theorem List.count_concat_self {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) :
        count a (l.concat a) = count a l + 1
        source
        @[simp]
        theorem List.count_pos_iff {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} :
        0 < count a l ↔ a ∈ l
        source
        @[reducible, inline, deprecated List.count_pos_iff (since := "2024-09-09")]
        abbrev List.count_pos_iff_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} :
        0 < count a l ↔ a ∈ l
        Equations
        Instances For
          source
          @[simp]
          theorem List.one_le_count_iff {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} :
          1 ≤ count a l ↔ a ∈ l
          source
          theorem List.count_eq_zero_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : ¬a ∈ l) :
          count a l = 0
          source
          theorem List.not_mem_of_count_eq_zero {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : count a l = 0) :
          ¬a ∈ l
          source
          theorem List.count_eq_zero {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} :
          count a l = 0 ↔ ¬a ∈ l
          source
          theorem List.count_eq_length {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} :
          count a l = l.length ↔ ∀ (b : α), b ∈ l → a = b
          source
          @[simp]
          theorem List.count_replicate_self {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (n : Nat) :
          count a (replicate n a) = n
          source
          theorem List.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
          theorem List.filter_beq {α : Type u_1} [BEq α] [LawfulBEq α] (l : List α) (a : α) :
          filter (fun (x : α) => x == a) l = replicate (count a l) a
          source
          theorem List.filter_eq {α : Type u_1} [DecidableEq α] (l : List α) (a : α) :
          filter (fun (x : α) => decide (x = a)) l = replicate (count a l) a
          source
          theorem List.le_count_iff_replicate_sublist {α : Type u_1} [BEq α] [LawfulBEq α] {n : Nat} {a : α} {l : List α} :
          n ≤ count a l ↔ (replicate n a).Sublist l
          source
          theorem List.replicate_count_eq_of_count_eq_length {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : count a l = l.length) :
          replicate (count a l) a = l
          source
          @[simp]
          theorem List.count_filter {α : Type u_1} [BEq α] [LawfulBEq α] {p : α → Bool} {a : α} {l : List α} (h : p a = true) :
          count a (filter p l) = count a l
          source
          theorem List.count_le_count_map {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} [DecidableEq β] (l : List α) (f : α → β) (x : α) :
          count x l ≤ count (f x) (map f l)
          source
          theorem List.count_filterMap {β : Type u_1} {α : Type u_2} [BEq β] (b : β) (f : α → Option β) (l : List α) :
          count b (filterMap f l) = countP (fun (a : α) => f a == some b) l
          source
          theorem List.count_flatMap {β : Type u_1} {α : Type u_2} [BEq β] (l : List α) (f : α → List β) (x : β) :
          count x (flatMap f l) = (map (count x ∘ f) l).sum
          source
          theorem List.count_erase {α : Type u_1} [BEq α] [LawfulBEq α] (a b : α) (l : List α) :
          count a (l.erase b) = count a l - if (b == a) = true then 1 else 0
          source
          @[simp]
          theorem List.count_erase_self {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) :
          count a (l.erase a) = count a l - 1
          source
          @[simp]
          theorem List.count_erase_of_ne {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} (ab : a ≠ b) (l : List α) :
          count a (l.erase b) = count a l