UniformLatticeFiniteGeneration.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Finite generation of a uniform lattice from metric chains

The bounded-distance lattice section sends ambient chains to bounded lattice steps. The steps belong to one finite ball, which therefore generates the lattice. This is the finite-generation part of the Švarc argument, proved from compactness and explicit chains.

theorem OAI.PolycyclicRecognition.IsUniformLattice.exists_generating_ball line 28
Source documentation
A uniform lattice in a metric group with linear metric chains has a finite generating set contained in a single induced metric ball.
```
theorem IsUniformLattice.exists_generating_ball {Λ : Subgroup G}
    (hΛ : IsUniformLattice Λ) (C : LinearMetricChains G) :
    ∃ B : ℝ, 0 ≤ B ∧
      Subgroup.closure (closedBall (1 : Λ) B) = ⊤ := by
…
```
theorem OAI.PolycyclicRecognition.IsUniformLattice.finitelyGenerated line 74
Source documentation
Compactness and linear ambient chains give finite generation without any algebraic structure theorem for lattices.
```
theorem IsUniformLattice.finitelyGenerated {Λ : Subgroup G}
    (hΛ : IsUniformLattice Λ) (C : LinearMetricChains G) : Group.FG Λ := by
…
```