Permutation Matching Equal-Size Subsets Inside a Finite Set

This is a finite-combinatorial auxiliary lemma.

Let $\Omega$ be finite and let $s,t,W\subseteq\Omega$ be finite subsets. Assume $s\subseteq W$, $t\subseteq W$, and $|s|=|t|$. Then there exists a permutation $\sigma$ of $\Omega$ such that $\sigma$ fixes every point outside $W$ and

The result supplies the permutation used to compare fibers of the image map on permutations supported inside $W$.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis.Tensor. Shown in its original module context. Proof omitted.

theorem exists_mem_fixingOutside_image_eq {W s t : Finset Ω} (hs : s ⊆ W) (ht : t ⊆ W)
    (hst : s.card = t.card) : ∃ σ ∈ fixingOutside W, s.image σ = t

Module navigation

Module: Analysis/Tensor/Symmetrization.

Previous: sum_norm_sq_le_sum_norm_sq_sum_subset · Next: apply_eq_of_image_eq.

Source excerpt, lines 464–465 · Frozen source 408915f.