The orders putting an element last

Reading a permutation σ of a finite linear order as an order of its elements, every order puts exactly one element of a nonempty set S last, and composing with the transposition of i and j exchanges the orders putting i last among S and those putting j last. So each i ∈ S is last among S for a 1 / #S fraction of the orders (Equiv.Perm.card_mul_card_filter_forall_le_eq_factorial).

Main results

• Equiv.Perm.card_filter_forall_le_eq: symmetry between elements of S being placed last.
• Equiv.Perm.card_mul_card_filter_forall_le_eq_factorial: each element of S is placed last by a 1 / #S fraction of all permutations.

theorem Equiv.Perm.card_filter_forall_le_eq {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] {S : Finset α} {i j : α} (hi : i ∈ S) (hj : j ∈ S) : {σ : Perm α | ∀ u ∈ S, σ u ≤ σ j}.card = {σ : Perm α | ∀ u ∈ S, σ u ≤ σ i}.card

As many orders put j ∈ S last among S as put i ∈ S last.

theorem Equiv.Perm.card_mul_card_filter_forall_le_eq_factorial {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] {S : Finset α} {i : α} (hi : i ∈ S) : S.card * {σ : Perm α | ∀ u ∈ S, σ u ≤ σ i}.card = (Fintype.card α).factorial

Each element of S is last among S for a 1 / #S fraction of the orders.