English
For a predicate p on Fin(n+1), the number of elements satisfying p is either count of successors plus 1 if p(0) is true, or just the count of successors if p(0) is false.
Русский
Для предиката p на Fin(n+1) число элементов, удовлетворяющих p, равно либо ∣{x: p(x.succ)}∣+1 при p(0)=истина, либо ∣{x: p(x.succ)}∣ при p(0)=ложь.
LaTeX
$$$ \\forall p:\\Fin(n+1)\\to \\mathrm{Prop} , [\\DecidablePred p] : \n\\#\\{x \\mid p x\\} = \\operatorname{ite}(p 0) (\\#\\{x \\mid p x.succ\\} + 1) (\\#\\{x \\mid p x.succ\\})$$$
Lean4
theorem card_filter_univ_succ (p : Fin (n + 1) → Prop) [DecidablePred p] :
#{x | p x} = if p 0 then #{x | p (.succ x)} + 1 else #{x | p (.succ x)} := by
rw [Fin.univ_succ, filter_cons, apply_ite Finset.card, card_cons, filter_map, card_map]; rfl
