English
Let n and a be natural numbers and p a predicate on natural numbers that is periodic with period a. Then the number of integers k with n ≤ k < n+a for which p(k) holds equals the number of residues r with 0 ≤ r < a for which p(r) holds.
Русский
Пусть n и a — натуральные числа, и p — предикат на натуральных числах, периодический с периодом a. Тогда число целых k с n ≤ k < n+a, для которых p(k) истинно, равно числу остатков r, удовлетворяющих 0 ≤ r < a и таким, что p(r) истинно.
LaTeX
$$$$\left| \{ k \in \mathbb{N} \mid n \le k < n+a,\ p(k) \} \right| = \left| \{ r \in \{0,1,\dots,a-1\} \mid p(r) \} \right|.$$$$
Lean4
/-- An interval of length `a` filtered over a periodic predicate of period `a` has cardinality
equal to the number naturals below `a` for which `p a` is true. -/
theorem filter_Ico_card_eq_of_periodic (n a : ℕ) (p : ℕ → Prop) [DecidablePred p] (pp : Periodic p a) :
((Ico n (n + a)).filter p).card = a.count p :=
filter_multiset_Ico_card_eq_of_periodic n a p pp
