CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-10-08

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Folner sequences for second countable compactly generated groups

Statement

Assume AC. Let $G$ be an amenable second countable compactly generated locally compact Hausdorff group (Amenable locally compact group, Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space, Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not) with fixed left Haar measure $μ$ (Left Haar integral and left Haar measure), and let $S \subseteq G$ be a compact generating set (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right, Topological group: multiplication and inversion are continuous) with $S = S^{- 1}$ containing $e$ and a nonempty open set. Then there is a sequence $(F_{n})_{n \geq 0}$ of Borel sets with $0 < μ (F_{n}) < \infty$ such that for every compact $Q \subseteq G$ $\lim_{n \to \infty} Δ_{Q} (F_{n}) = 0, Δ_{Q} (F) : = \sup ({0} \cup {μ (x F △ F) / μ (F) : x \in Q}) .$ Thus $Δ_{\emptyset} (F) = 0$ . Such a sequence is a Følner sequence for $G$ . Conversely, a locally compact Hausdorff group with such a sequence satisfies the left Følner condition (Left Følner nets for locally compact groups) and hence is amenable, so for such a group amenability is equivalent to the existence of a Følner sequence. Only compact generation, not second countability, is used by the construction.

Facts & Assumptions

Given: AC; a locally compact Hausdorff group $G$ with fixed left Haar measure $μ$ ; the amenability of $G$ ; a compact generating set $S \subseteq G$ with $S = S^{- 1}$ containing $e$ and a nonempty open set $U \subseteq S$ , with $G = ⋃_{n \geq 1} S^{n}$ .

[A1]

AC implies AC $_{ω}$ : for a sequence $(X_{n})_{n \in N}$ of nonempty sets one applies AC to the family ${X_{n} : n \in N}$ and evaluates the resulting selector at each $X_{n}$ (The Axiom of Choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

Under AC, $G$ is amenable, meaning that there is a left-invariant mean $m$ on $L^{\infty} (G)$ (Amenable locally compact group), if and only if $G$ satisfies the left Følner condition: for every compact $Q \subseteq G$ and every $ε > 0$ there is a Borel set $F \subseteq G$ with $0 < μ (F) < \infty$ and $Δ_{Q} (F) \leq ε$ (The Følner criterion for locally compact groups).

[F2]

For a Borel set $F \subseteq G$ with $0 < μ (F) < \infty$ and compact $Q \subseteq G$ one has $Δ_{Q} (F) = \sup ({0} \cup {μ (x F △ F) / μ (F) : x \in Q})$ , so in particular $Δ_{\emptyset} (F) = 0$ (Left Følner nets for locally compact groups).

[F3]

Multiplication $(x, y) \mapsto x y$ and inversion $x \mapsto x^{- 1}$ are continuous on $G$ ; finite products of compact spaces are compact; and continuous images of compact sets are compact (Topological group: multiplication and inversion are continuous, A product of finitely many compact spaces is compact in the product topology, A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism).

[F4]

Every ambient open cover of a compact subspace has a finite subcover (A subspace is compact exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it).

Proof

Given: AC; a locally compact Hausdorff group $G$ with fixed left Haar measure $μ$ ; the amenability of $G$ ; a compact generating set $S = S^{- 1} ∋ e$ containing the nonempty open set $U \subseteq S$ , with $G = ⋃_{n \geq 1} S^{n}$ .

Proof technique: direct.

1.1F3given

For $n \geq 1$ put $K_{n} : = S^{n} = {s_{1} \dots s_{n} : s_{1}, \dots, s_{n} \in S}$ . The map $(s_{1}, \dots, s_{n}) \mapsto s_{1} \dots s_{n}$ is continuous from the finite product $S \times \dots \times S$ , which is compact, onto $K_{n}$ , so $K_{n}$ is compact; and $K_{n} \subseteq K_{n + 1}$ because $e \in S$ .

1.2F1F2algebra

For the reverse implication suppose that $(F_{n})_{n \geq 0}$ is a sequence of Borel sets with $0 < μ (F_{n}) < \infty$ for which $Δ_{Q} (F_{n})$ tends to $0$ for every compact $Q \subseteq G$ . Given a compact $Q$ and $ε > 0$ , the convergence to $0$ gives $n_{1}$ with $Δ_{Q} (F_{n}) \leq ε$ for every $n \geq n_{1}$ ; then $F : = F_{n_{1}}$ is Borel with $0 < μ (F) < \infty$ and $Δ_{Q} (F) \leq ε$ by [F2]. Thus $G$ satisfies the left Følner condition, and [F1] makes $G$ amenable.

2.1F3F4step 1.1givenconstruct

Put $W : = U \cdot U^{- 1}$ . Then $W$ is open, being a union of translates of the open set $U \subseteq S$ ; $e \in W$ because $e = u \cdot u^{- 1}$ for any $u \in U$ ; and $W \subseteq S \cdot S^{- 1} = S^{2}$ because $U \subseteq S = S^{- 1}$ . For $y \in S^{m}$ the translate $y W$ is open and contains $y = y e$ , while $y W \subseteq S^{m} S^{2} = S^{m + 2}$ ; hence $S^{m} \subseteq int (S^{m + 2})$ for every $m \geq 1$ . Therefore the open sets $int (K_{2 n}) = int (S^{2 n})$ increase, and they cover $G$ : for $x \in S^{m}$ padding with $e \in S$ gives $x \in S^{2 m} \subseteq int (S^{2 m + 2}) = int (K_{2 m + 2})$ , so $x$ lies in the member of index $m + 1$ . If $Q = \emptyset$ , take $n_{0} = 1$ . Otherwise [F4] gives a finite subcover of the compact $Q \subseteq G$ by these ambient open sets; taking the largest index gives $n_{0}$ with $Q \subseteq int (K_{2 n_{0}}) \subseteq K_{2 n_{0}}$ , and step 1.1 gives $Q \subseteq K_{n}$ for all $n \geq 2 n_{0}$ .

2.2A1F1F2step 1.1choose

For each $n \geq 0$ , [F1] applied to the compact set $K_{n + 1}$ with tolerance $1 / (n + 1)$ produces a Borel set $F$ with $0 < μ (F) < \infty$ and $Δ_{K_{n + 1}} (F) \leq 1 / (n + 1)$ , so the family of all such witnesses is nonempty; by [A1] choose a sequence $(F_{n})_{n \geq 0}$ in which $F_{n}$ is a witness for $K_{n + 1}$ at tolerance $1 / (n + 1)$ , so each $F_{n}$ is Borel with $0 < μ (F_{n}) < \infty$ and $Δ_{K_{n + 1}} (F_{n}) \leq 1 / (n + 1)$ .

3.1F2step 2.1step 2.2algebra

Let $Q \subseteq G$ be compact and choose $m$ as in step 2.1, so $Q \subseteq K_{r}$ for all $r \geq 2 m$ . For every $n \geq 2 m - 1$ , one has $Q \subseteq K_{n + 1}$ , so the family defining $Δ_{Q} (F_{n})$ is contained in the family defining $Δ_{K_{n + 1}} (F_{n})$ , hence $0 \leq Δ_{Q} (F_{n}) \leq Δ_{K_{n + 1}} (F_{n}) \leq 1 / (n + 1)$ by step 2.2. This also covers $Q = \emptyset$ because both families include $0$ . Thus $Δ_{Q} (F_{n}) \to 0$ and $(F_{n})$ is a Følner sequence.

4.1A1F1step 3.1step 1.2∎

Steps 1.1, 2.1, 2.2, and 3.1 produce a Følner sequence for an amenable $G$ from the compact sets $S^{n}$ and their open exhaustion of $G$ , and step 1.2 reverses the implication, giving the stated equivalence; the construction never uses second countability, and the stated AC is spent only through the criterion in [F1] and the countable selection in [A1].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

67 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Bachir Bekka, Pierre de la Harpe and Alain Valette, Kazhdan's Property (T) (Cambridge University Press, 2008; author-hosted complete text) (standard reference, not scraped)
Anne Thomas, The Banach-Tarski Paradox and Amenability, Lecture 19: Reiter's Property and the Folner Condition (University of Sydney Honours lecture notes, 9 October 2012) (standard reference, not scraped)