English
Let n and a be natural numbers and p a decidable predicate with period a. The cardinality of the filtered interval Ico n (n+a) is exactly a.count p.
Русский
Пусть n и a натуральны, p — разрешимый предикат периодический с периодом a. Кардинальность множества, полученного фильтрацией по p на интервале Ico n (n+a), равна a.count p.
LaTeX
$$$ \operatorname{card}(\operatorname{filter} p (\operatorname{Ico} n (n+a))) = \operatorname{count} p a $$$
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_multiset_Ico_card_eq_of_periodic (n a : ℕ) (p : ℕ → Prop) [DecidablePred p] (pp : Periodic p a) :
card (filter p (Ico n (n + a))) = a.count p :=
by
rw [count_eq_card_filter_range, Finset.card, Finset.filter_val, Finset.range_val, ← multiset_Ico_map_mod n, ←
map_count_True_eq_filter_card, ← map_count_True_eq_filter_card, map_map]
congr; funext n
exact (Function.Periodic.map_mod_nat pp n).symm
