A fixed-point-free involution halves a finset

A finset carrying a fixed-point-free involution is the disjoint union of two-element orbits, so its cardinality is even, and the same holds of a finite type (even_fintypeCard_of_involution). This is the counting behind every parity statement about matched flags: edges match flags in pairs, chords match labels in pairs, and a directed matching matches its points in pairs.

theorem RS.even_card_of_involution {γ : Type} (t : Finset γ) (i : γ → γ) : (∀ x ∈ t, i x ∈ t) → (∀ x ∈ t, i (i x) = x) → (∀ x ∈ t, i x ≠ x) → Even t.card

A fixed-point-free involution halves a finset.

theorem RS.even_fintypeCard_of_involution {X : Type} [Fintype X] (i : X → X) (hinv : ∀ (x : X), i (i x) = x) (hne : ∀ (x : X), i x ≠ x) : Even (Fintype.card X)

The Fintype form: a type carrying a fixed-point-free involution has even cardinality.