Counting a subtype of a sum

The elements of β ⊕ γ satisfying a predicate are those of β and those of γ that satisfy it (Nat.card_subtype_sum); along a decomposition α ≃ β ⊕ γ the same count splits a subtype of α (Nat.card_subtype_eq_add_of_equiv_sum).

Main results

• Nat.card_subtype_sum: counting a subtype of a sum.
• Nat.card_subtype_eq_add_of_equiv_sum: counting a subtype along a decomposition into a sum.

theorem Nat.card_subtype_sum {β : Type u_2} {γ : Type u_3} [Finite β] [Finite γ] (P : β ⊕ γ → Prop) : Nat.card { x : β ⊕ γ // P x } = Nat.card { b : β // P (Sum.inl b) } + Nat.card { c : γ // P (Sum.inr c) }

The elements of β ⊕ γ satisfying P are those of β and those of γ that satisfy it.

theorem Nat.card_subtype_eq_add_of_equiv_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Finite β] [Finite γ] (e : α ≃ β ⊕ γ) (P : α → Prop) : Nat.card { a : α // P a } = Nat.card { b : β // P (e.symm (Sum.inl b)) } + Nat.card { c : γ // P (e.symm (Sum.inr c)) }

Counting along a decomposition α ≃ β ⊕ γ: the elements satisfying P are those coming from β and those coming from γ.