List.count_pos_iff_mem
theorem List.count_pos_iff_mem :
∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {l : List α}, 0 < List.count a l ↔ a ∈ l
This theorem, `List.count_pos_iff_mem`, states that for any type `α` with decidable equality and any element `a` of type `α` and any list `l` of elements of type `α`, the count of `a` in `l` is greater than 0 if and only if `a` is a member of `l`. In other words, an element `a` is in the list `l` if and only if there is at least one occurrence of `a` in `l`.
More concisely: For any type `α` with decidable equality, an element `a` is in list `l` of type `α` if and only if the count of `a` in `l` is greater than 0.
|
List.count_cons
theorem List.count_cons :
∀ {α : Type u_1} [inst : DecidableEq α] (a b : α) (l : List α),
List.count a (b :: l) = List.count a l + if a = b then 1 else 0
This theorem, `List.count_cons`, states that for any type `α` that has decidable equality and for any elements `a` and `b` of this type and a list `l` of elements of the same type, the count of the element `a` in the list formed by consing `b` to `l` i.e., `b :: l`, is equal to the count of `a` in the original list `l` plus 1 if `a` is equal to `b`, and plus 0 otherwise. In other words, it determines how the count of an element in a list changes when a new element is added to the front of the list. If the new element is same as the one being counted, it increases the count by one, otherwise the count remains the same.
More concisely: For any type `α` with decidable equality and list `l` of elements `α`, the count of an element `a` in the list `b :: l` is `if a = b then succ (count a l) else count a l`.
|
List.countP_cons_of_neg
theorem List.countP_cons_of_neg :
∀ {α : Type u_1} (p : α → Bool) {a : α} (l : List α), ¬p a = true → List.countP p (a :: l) = List.countP p l := by
sorry
This theorem states that for any type `α`, any function `p` from `α` to Boolean values, any element `a` of type `α`, and any list `l` of elements of type `α`, if `p a` is not true, then the count of elements in the list obtained by prepending `a` to `l` that satisfies `p`, `List.countP p (a :: l)`, equals the count of elements in `l` that satisfies `p`, `List.countP p l`. In other words, if a given predicate `p` does not hold for an element `a`, then adding `a` to the front of a list `l` does not change the number of elements in the list for which the predicate `p` holds.
More concisely: If `p(a)` is false, then the number of elements in the list `a :: l` satisfying `p` equals the number of elements in list `l` satisfying `p`.
|
List.length_eq_countP_add_countP
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
The theorem `List.length_eq_countP_add_countP` states that for any list `l` of elements of some type `α` and any predicate `p` mapping elements of `α` to boolean values, the length of the list `l` is equal to the sum of the counts of elements of `l` that satisfy the predicate `p` and the elements of `l` that do not satisfy the predicate `p`. In other words, it shows that the total number of elements in a list is equal to the number of elements that pass a certain condition plus the number of elements that fail the same condition.
In mathematical terms, if we denote with `|l|` the length of the list `l`, with `#p(l)` the count of elements satisfying the predicate `p`, and with `#¬p(l)` the count of elements not satisfying `p`, the theorem can be expressed as `|l| = #p(l) + #¬p(l)`.
More concisely: The length of a list equals the number of elements satisfying a given predicate plus the number of elements not satisfying it.
|
List.countP_cons
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
The given theorem, `List.countP_cons`, states that for any type `α`, any predicate `p` that is a function from type `α` to `Bool`, any element `a` of type `α`, and any list `l` of elements of type `α`, the count of elements satisfying the predicate `p` in the list that results from prepending the element `a` to the list `l` (`a :: l`) is equal to the count of elements satisfying `p` in `l` plus 1 if `a` satisfies `p` (`if p a = true then 1 else 0`). In other words, if `a` is a member of the list that satisfies the predicate `p`, it is counted as 1, otherwise as 0, and this is added to the count of elements in the original list satisfying `p`.
More concisely: For any type `α`, predicate `p` on `α`, element `a ∈ α`, and list `l ∈ List α`, the number of elements in `l` satisfying `p` is equal to the number of elements in `a :: l` satisfying `p` if `p(a)` is true, otherwise it is one more than the number of elements in `l` satisfying `p`.
|
List.filter_eq
theorem List.filter_eq :
∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (a : α),
List.filter (fun x => decide (x = a)) l = List.replicate (List.count a l) a
This theorem states that for any given list `l` of elements of type `α` (with decidable equality) and any given element `a` from the same type `α`, the list obtained by filtering `l` such that it only contains elements that are equal to `a`, is equivalent to a list that replicates `a` a number of times equal to the count of `a` in the original list `l`. In simpler terms, if you filter a list to only include instances of a certain element, the resulting list is the same as if you just replicated that element for the number of times it originally appeared in the list.
More concisely: For any list `l` of decidably equal elements `α` and any `a` in `α`, the list obtained by filtering `l` equal to `a` is equal to the repeated list of length equal to the count of `a` in `l`.
|
List.count_cons_self
theorem List.count_cons_self :
∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (l : List α), List.count a (a :: l) = List.count a l + 1
The theorem `List.count_cons_self` states that for any type `α` that has decidable equality and for any element `a` of type `α` and list `l` of elements of type `α`, the count of `a` in the list formed by prepending `a` to `l` is equal to the count of `a` in `l` plus one. In other words, if you add an element to the start of a list, the count of that element in the new list increases by one.
More concisely: For any type `α` with decidable equality and list `l` of elements from `α`, the number of occurrences of an element `a` in the list `a :: l` is one more than the number of occurrences of `a` in `l`.
|
List.count_replicate_self
theorem List.count_replicate_self :
∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (n : ℕ), List.count a (List.replicate n a) = n
The theorem `List.count_replicate_self` states that for any type `α` with decidable equality and for any element `a` of type `α` and a natural number `n`, the count of `a` in a list that is created by replicating `a` `n` times is precisely `n`. In simpler words, it expresses that the number of occurrences of a specific value in a list, which is formed by repeating that value a certain number of times, is equal to that number of repetitions.
More concisely: For any type `α` with decidable equality and natural number `n`, the length of the list obtained by replicating an element `a` of type `α` `n` times equals `n`.
|
List.countP_append
theorem List.countP_append :
∀ {α : Type u_1} (p : α → Bool) (l₁ l₂ : List α), List.countP p (l₁ ++ l₂) = List.countP p l₁ + List.countP p l₂
This theorem, `List.countP_append`, states that for any type `α`, any function `p` from `α` to `Bool`, and any two lists `l₁` and `l₂` of type `α`, the number of elements in the concatenation of `l₁` and `l₂` that satisfy `p` is equal to the sum of the number of elements in `l₁` that satisfy `p` and the number of elements in `l₂` that satisfy `p`. Essentially, if we split a list into two parts, the total number of elements that satisfy a given condition `p` in the combined list is the same as the sum of the elements satisfying `p` in each of the individual lists.
More concisely: For any type `α`, function `p` from `α` to `Bool`, and lists `l₁` and `l₂` of type `α`, `List.countP (l₁ ++ l₂) p = List.countP l₁ p + List.countP l₂ p`.
|
List.count_cons_of_ne
theorem List.count_cons_of_ne :
∀ {α : Type u_1} [inst : DecidableEq α] {a b : α}, a ≠ b → ∀ (l : List α), List.count a (b :: l) = List.count a l
This theorem states that for any type `α` with decidable equality (`DecidableEq α`), given two elements `a` and `b` of this type such that `a ≠ b`, and given a list `l` of elements of type `α`, the number of occurrences of `a` in the list that is obtained by prepending `b` to `l` (`b :: l`) is equal to the number of occurrences of `a` in the original list `l`. In other words, prepending an element not equal to `a` to the list does not change the count of `a` in the list.
More concisely: For any type `α` with decidable equality, and any `a ≠ b` in `α`, the number of occurrences of `a` in the list `b :: l` is equal to the number of occurrences of `a` in the list `l`.
|
List.le_count_iff_replicate_sublist
theorem List.le_count_iff_replicate_sublist :
∀ {α : Type u_1} [inst : DecidableEq α] {n : ℕ} {a : α} {l : List α},
n ≤ List.count a l ↔ (List.replicate n a).Sublist l
The theorem `List.le_count_iff_replicate_sublist` states that for any type `α` with decidable equality, any natural number `n`, any value `a` of type `α`, and any list `l` of elements of type `α`, the count of `a` in `l` is greater than or equal to `n` if and only if the list that consists of `n` copies of `a` is a sublist of `l`. In other words, having at least `n` occurrences of `a` in `l` is equivalent to the condition that `n` copies of `a` form a sublist of `l`.
More concisely: For any type `α` with decidable equality, natural number `n`, value `a` of type `α`, and list `l` of elements of type `α`, the number of occurrences of `a` in `l` is greater than or equal to `n` if and only if `l` has `n` consecutive elements equal to `a`.
|
List.count_append
theorem List.count_append :
∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (l₁ l₂ : List α),
List.count a (l₁ ++ l₂) = List.count a l₁ + List.count a l₂
The theorem `List.count_append` states that for any type `α` with decidable equality, for any element `a` of type `α`, and for any two lists `l₁` and `l₂` of type `α`, the number of occurrences of `a` in the concatenation of `l₁` and `l₂` is equal to the sum of the number of occurrences of `a` in `l₁` and the number of occurrences of `a` in `l₂`. In other words, counting an element in the combined list is equivalent to counting the element in each list separately and adding the results.
More concisely: For any type `α` with decidable equality, the number of occurrences of an element `a` in the concatenation of lists `l₁` and `l₂` equals the sum of the number of occurrences of `a` in `l₁` and the number of occurrences of `a` in `l₂`.
|
List.countP_cons_of_pos
theorem List.countP_cons_of_pos :
∀ {α : Type u_1} (p : α → Bool) {a : α} (l : List α), p a = true → List.countP p (a :: l) = List.countP p l + 1
This theorem is about counting the elements in a list that satisfy a certain condition. For any type `α`, any function `p` from `α` to `Bool`, any element `a` of type `α`, and any list `l` of elements of type `α`, if the function `p` applied to `a` equals `true`, then the count of elements in the list `a :: l` that satisfy `p` is equal to the count of elements in `l` that satisfy `p`, plus one. This is because the element `a` is added to the beginning of the list `l`, and it satisfies the condition `p`.
More concisely: For any type `α`, list `l` of `α`, element `a` of `α`, and function `p` from `α` to `Bool`, if `p(a) = true`, then the number of elements in `l` satisfying `p` is equal to the number of elements in `a :: l` satisfying `p`.
|
List.countP_eq_length_filter
theorem List.countP_eq_length_filter :
∀ {α : Type u_1} (p : α → Bool) (l : List α), List.countP p l = (List.filter p l).length
The theorem `List.countP_eq_length_filter` states that for any type `α`, any predicate `p` of type `α → Bool`, and any list `l` of type `List α`, the count of elements in `l` that satisfy the predicate `p` is equal to the length of the list obtained by filtering `l` with the predicate `p`. This is, in mathematical terms, if we denote by $p$ a certain property and by $l$ a list of elements, the number of elements of $l$ having the property $p$ is the same as the number of elements in the filtered list where the filter criteria is the property $p$.
More concisely: For any type `α`, predicate `p` on `α`, and list `l` of length `n` over `α`, the number of elements in `l` satisfying `p` equals the length of the filtered list `l.filter p`.
|
List.count_eq_zero_of_not_mem
theorem List.count_eq_zero_of_not_mem :
∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {l : List α}, a ∉ l → List.count a l = 0
This theorem states that for any type `α` that has a decidable equality, any element `a` of type `α` and any list `l` of elements of type `α`, if the element `a` is not an element of the list `l`, then the count of `a` in `l` is zero. In other words, if `a` is not in `l`, `a` occurs zero times in `l`.
More concisely: For any decidably equal type `α` and list `l` of elements from `α`, if `a` is not an element of `l`, then the count of `a` in `l` equals zero.
|