UniformLatticeQuotient.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Compact quotient and compact fundamental cover

The concrete uniform lattice definition agrees with the usual compact-coset- quotient definition. Left and right cosets are interchanged by inversion.

theorem OAI.PolycyclicRecognition.IsUniformLattice.compactSpace_quotient line 23
Source documentation
The compact fundamental cover gives compactness of the ordinary right coset quotient, without any normality assumption.
```
theorem IsUniformLattice.compactSpace_quotient {Λ : Subgroup G}
    (hΛ : IsUniformLattice Λ) : CompactSpace (G ⧸ Λ) := by
…
```
theorem OAI.PolycyclicRecognition.isUniformLattice_of_compact_quotient line 48
Source documentation
In a locally compact group, a compact coset quotient admits a compact fundamental cover. The finite subcover consists of images of relatively compact neighborhoods.
```
theorem isUniformLattice_of_compact_quotient [LocallyCompactSpace G]
    (Λ : Subgroup G) [DiscreteTopology Λ] [CompactSpace (G ⧸ Λ)] :
    IsUniformLattice Λ := by
…
```

theorem OAI.PolycyclicRecognition.isUniformLattice_iff_compact_quotient line 73

Source documentation

This is the usual uniform-lattice predicate in locally compact groups.

theorem isUniformLattice_iff_compact_quotient [LocallyCompactSpace G] (Λ : Subgroup G) :
    IsUniformLattice Λ ↔ DiscreteTopology Λ ∧ CompactSpace (G ⧸ Λ) := by
…