Mathlib.Data.Nat.Periodic._auxLemma.1
theorem Mathlib.Data.Nat.Periodic._auxLemma.1 : ∀ {b : Prop} (α : Sort u_1) [i : Nonempty α], (α → b) = b
This theorem states that for any proposition `b` and any type `α` (which is nonempty, meaning there exists at least one value of type `α`), the type of a function that takes an input of type `α` and returns `b` is simply the same as the type of `b`. In other words, if `b` is any proposition and `α` is any nonempty type, then the function type `(α → b)` collapses to `b`.
More concisely: For any nonempty type `α` and proposition `b`, the function type `(α → b)` is equivalent to `b`.
|
Nat.filter_multiset_Ico_card_eq_of_periodic
theorem Nat.filter_multiset_Ico_card_eq_of_periodic :
∀ (n a : ℕ) (p : ℕ → Prop) [inst : DecidablePred p],
Function.Periodic p a → Multiset.card (Multiset.filter p (Multiset.Ico n (n + a))) = Nat.count p a
This theorem states that for any natural numbers `n` and `a`, and any decidable predicate `p` on natural numbers, if `p` is a periodic function with period `a`, then the cardinality of the multiset obtained by filtering the closed-open interval from `n` to `n + a` with `p` is equal to the number of natural numbers less than `a` for which `p` holds true. In other words, for a periodic predicate, the count of `true` instances in an interval of length equal to its period is constant, no matter the starting point of the interval.
More concisely: For any natural numbers n, a, and a decidable periodic function p on natural numbers, the cardinality of the multiset of numbers in the interval [n, n + a) where p holds is equal to the number of natural numbers less than a with p(x) = true.
|
Nat.filter_Ico_card_eq_of_periodic
theorem Nat.filter_Ico_card_eq_of_periodic :
∀ (n a : ℕ) (p : ℕ → Prop) [inst : DecidablePred p],
Function.Periodic p a → (Finset.filter p (Finset.Ico n (n + a))).card = Nat.count p a
This theorem, named `Nat.filter_Ico_card_eq_of_periodic`, states that for any natural numbers `n` and `a`, and a decidable predicate `p`, if `p` is a periodic function with period `a`, then the cardinality of the set that results from filtering the interval from `n` to `n + a` (with `n + a` exclusive) according to the predicate `p` is equal to the count of natural numbers less than `a` for which `p` is true. In other words, within a specific interval of length `a`, the number of elements satisfying the predicate `p` is the same as the number of naturals below `a` that satisfy `p`, given that `p` repeats itself every `a` steps.
More concisely: For any natural number `n`, natural number `a`, and decidable predicate `p` that is periodic with period `a`, the cardinality of the filtered set `{x | x ∈ Nat, n ≤ x < n + a} with p` is equal to the count of natural numbers less than `a` that satisfy `p`.
|