Matching minimal covering nets of a compact group (source code)

= Matching minimal covering nets of a compact group
{title2=$F\leftrightarrow F',\quad f^{-1}\pi(f)\in VV^{-1}$}

Two minimal left covering nets for the same identity neighbourhood $V$ can be matched bijectively so that paired translates intersect. Join $f\in F$ to $f'\in F'$ when $fV\cap f'V\ne\varnothing$. For $S\subseteq F$, its neighbours $N(S)$ cover every point covered by $S$, so $(F\setminus S)\cup N(S)$ still covers the group. Minimality forces $|N(S)|\geq|S|$. <Hall's marriage theorem> supplies the matching, and an intersection $fv=f'v'$ gives $f^{-1}f'=vv'^{-1}\in VV^{-1}$. Averaging a continuous function over matched nets therefore gives values differing by at most its uniform oscillation on right displacements in $VV^{-1}$. This is the finite combinatorial step in constructing <Haar measure> on a compact group.