erdos_ko_rado_permutations
Provedcombinatoricspermutationsproved
Erdős–Ko–Rado for permutations: An intersecting family of permutations of {1,...,n} has size at most (n-1)!. Proved by Deza–Frankl (1983). The analogous result for t-intersecting families with sharper bounds is still studied.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem erdos_ko_rado_permutations (n : ℕ) (hn : 2 ≤ n)
(F : Finset (Equiv.Perm (Fin n)))
(hint : ∀ sigma ∈ F, ∀ tau ∈ F, ∃ i : Fin n, sigma i = tau i) :
F.card ≤ (n - 1).factorial := by
sorrySource