EVEN CARDINALITY FROM A FIXED-POINT-FREE INVOLUTION

A finite set closed under a fixed-point-free involution has even cardinality. This is the small combinatorial lemma later used in the Catalan recurrence.

theorem even_card_of_fpf_closed {α : Type u_1} {p : Equiv.Perm α} (hinv : ∀ (x : α), p (p x) = x) (hfpf : ∀ (x : α), p x ≠ x) (S : Finset α) (h_closed : ∀ x ∈ S, p x ∈ S) : Even S.card

A finite set closed under a fixed-point-free involution has even cardinality.

Proof by strong induction: pick any x ∈ S, remove the pair {x, p x}, show the remainder is still closed under p, and recurse.