Nat.count_succ_eq_count
theorem Nat.count_succ_eq_count :
∀ {p : ℕ → Prop} [inst : DecidablePred p] {n : ℕ}, ¬p n → Nat.count p (n + 1) = Nat.count p n
This theorem, `Nat.count_succ_eq_count`, states that for any natural number `n` and any decidable predicate `p`, if `n` does not satisfy the predicate `p`, then the count of natural numbers less than `n + 1` that satisfy `p` equals to the count of natural numbers less than `n` that satisfy `p`. In other words, adding 1 to `n` doesn't increase the count of natural numbers satisfying `p` if `n` itself does not satisfy `p`.
More concisely: If `n` is a natural number and `p` is a decidable predicate such that `n` does not satisfy `p`, then the number of natural numbers less than `n + 1` that satisfy `p` equals the number of natural numbers less than `n` that satisfy `p`.
|
Nat.count_succ_eq_succ_count
theorem Nat.count_succ_eq_succ_count :
∀ {p : ℕ → Prop} [inst : DecidablePred p] {n : ℕ}, p n → Nat.count p (n + 1) = Nat.count p n + 1
The theorem `Nat.count_succ_eq_succ_count` states that for all decidable predicates `p` mapping natural numbers to propositions and for any natural number `n`, if the predicate `p` holds true for `n`, then the count of natural numbers less than `n + 1` satisfying `p` is equal to the count of natural numbers less than `n` satisfying `p` plus one. In other words, if a number `n` satisfies a given predicate, including this number in the count increases the total by one.
More concisely: For any decidable predicate `p` on natural numbers, if `n` has `p` holding at `n`, then the number of natural numbers less than `n + 1` satisfying `p` equals the number of natural numbers less than `n` satisfying `p` plus one.
|
Nat.count_monotone
theorem Nat.count_monotone : ∀ (p : ℕ → Prop) [inst : DecidablePred p], Monotone (Nat.count p)
The theorem `Nat.count_monotone` states that for any decidable predicate `p` on natural numbers, the function `Nat.count p` is monotone. In other words, if `m` and `n` are natural numbers and `m ≤ n`, then the number of natural numbers less than `m` that satisfy `p` is less than or equal to the number of natural numbers less than `n` that satisfy `p`. This property is known as monotonicity.
More concisely: For any decidable predicate `p` on natural numbers, the function `Nat.count p` is monotone, that is, `Nat.count p x ≤ Nat.count p y` whenever `x ≤ y`.
|
Nat.count_eq_card_filter_range
theorem Nat.count_eq_card_filter_range :
∀ (p : ℕ → Prop) [inst : DecidablePred p] (n : ℕ), Nat.count p n = (Finset.filter p (Finset.range n)).card := by
sorry
This theorem states that for any given predicate `p` on natural numbers that is decidable and any natural number `n`, the count of natural numbers `k` less than `n` that satisfy the predicate `p` is equal to the cardinality (size) of the set obtained by filtering the set of natural numbers less than `n` (represented as a finite set) according to the predicate `p`. In other words, it establishes an equivalence between counting elements that satisfy a predicate in a list and filtering those elements in a set.
More concisely: For any decidable predicate `p` on natural numbers, the number of natural numbers less than `n` satisfying `p` is equal to the size of the filter of natural numbers less than `n` that satisfy `p`.
|
Nat.count_succ
theorem Nat.count_succ :
∀ (p : ℕ → Prop) [inst : DecidablePred p] (n : ℕ), Nat.count p (n + 1) = Nat.count p n + if p n then 1 else 0 := by
sorry
This theorem, `Nat.count_succ`, states that for any natural number `n` and any decidable predicate `p` (a function from natural numbers to propositions that we can decide whether it's true or false), the count of natural numbers less than `n + 1` that satisfy the predicate `p` is equal to the count of natural numbers less than `n` that satisfy `p`, plus 1 if `n` itself satisfies `p`, and plus 0 otherwise. Essentially, it is considering whether the next number, `n`, should be included in the count based on if it satisfies the predicate `p`.
More concisely: The number of natural numbers less than `n + 1` satisfying a decidable predicate `p` is equal to the count of those less than `n` satisfying `p` plus 1 if `n` satisfies `p`, or equal to the count of those less than `n` satisfying `p` otherwise.
|
Nat.count_eq_card_fintype
theorem Nat.count_eq_card_fintype :
∀ (p : ℕ → Prop) [inst : DecidablePred p] (n : ℕ), Nat.count p n = Fintype.card { k // k < n ∧ p k }
The theorem `Nat.count_eq_card_fintype` states that for any decidable predicate `p` on natural numbers, and for any natural number `n`, the count of natural numbers less than `n` that satisfy the predicate `p` is equal to the cardinality of the set of all numbers `k` such that `k` is less than `n` and `k` satisfies the predicate `p`. In other words, it shows a correspondence between counting the number of elements less than `n` satisfying a condition and the size of a finite set of elements satisfying the same condition and being less than `n`.
More concisely: For any decidable predicate `p` on natural numbers, the number of natural numbers less than `n` satisfying `p` equals the cardinality of the finite set of natural numbers less than `n` that satisfy `p`.
|