Counting the permutations that fix a set

The permutations of a finite type α that fix every point of a set U are the permutations of the complement of U, so there are (#α - #U)! of them (Equiv.Perm.card_filter_forall_eq_self). More generally, if f is injective on U, then (#α - #U)! permutations agree with f on U: composing with one such permutation τ (Equiv.extendSubtype) matches them with the permutations fixing U.

Main results

• Equiv.Perm.card_filter_forall_eq_self: (#α - #U)! permutations fix every point of U.
• Equiv.Perm.card_filter_forall_eq_of_injOn: (#α - #U)! permutations agree on U with a function injective on U.

theorem Equiv.Perm.card_filter_forall_eq_self {α : Type u_1} [Fintype α] [DecidableEq α] (U : Finset α) : {τ : Perm α | ∀ u ∈ U, τ u = u}.card = (Fintype.card α - U.card).factorial

The permutations fixing a set of a finite type α number (#α - #U)!.

theorem Equiv.Perm.card_filter_forall_eq_of_injOn {α : Type u_1} [Fintype α] [DecidableEq α] (U : Finset α) (f : α → α) (hf : Set.InjOn f ↑U) : {σ : Perm α | ∀ u ∈ U, σ u = f u}.card = (Fintype.card α - U.card).factorial

The permutations extending an injective map on a set U of a finite type α number (#α - #U)!.