Counting in an appended tuple

The number of entries of Fin.append x y satisfying a predicate is the number for x plus the number for y.

Main results

• Fin.card_filter_append: counting entries satisfying a predicate across Fin.append.

theorem Fin.card_filter_append {α : Type u_1} {m p : ℕ} (P : α → Prop) [DecidablePred P] (x : Fin m → α) (y : Fin p → α) : {i : Fin (m + p) | P (append x y i)}.card = {i : Fin m | P (x i)}.card + {j : Fin p | P (y j)}.card

The entries of Fin.append x y satisfying P are those of x and those of y.