Symmetric differences of translates of finite sets #
An element g acting injectively on a type X (for example, any element of a group acting on
X) moves a finite set F ⊆ X to a translate g • F of the same size, so g • F has as many
points outside F as F has outside g • F. Hence the symmetric difference g • F ∆ F has
twice as many points as g • F \ F. Følner-type arguments use this to pass between symmetric
differences and one-sided differences.
Main results #
Finset.card_smul_finset_symmDiff:|gF △ F| = 2 |gF \ F|for a finite setF.
theorem
Finset.card_smul_finset_symmDiff
{G : Type u_1}
{X : Type u_2}
[SMul G X]
[IsLeftCancelSMul G X]
[DecidableEq X]
(g : G)
(F : Finset X)
:
A translate g • F of a finite set has as many points outside F as F has outside g • F,
so its symmetric difference with F has twice as many points as g • F \ F.