Images of Subsets Under Supported Permutations

This is a finite-set invariance lemma.

Let $A,Q\subseteq\Omega$ be finite subsets with $A\subseteq Q$. If a permutation $\sigma$ fixes every point outside $Q$, then the image $\sigma(A)$ is a subset of $Q$ with the same cardinality as $A$:

This identifies the possible images of $A$ when permutation sums are restricted to permutations supported in $Q$.

Original Lean declaration header

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

theorem image_mem_powersetCard_of_mem_fixingOutside {A Q : Finset Ω} (hAQ : A ⊆ Q)
    {σ : Equiv.Perm Ω} (hσ : σ ∈ fixingOutside Q) : A.image σ ∈ Q.powersetCard A.card

Module navigation

Module: Analysis/Tensor/Symmetrization.

Previous: apply_eq_of_image_eq · Next: card_fiber_eq.

Source excerpt, lines 717–718 · Frozen source 408915f.