ConstructChainMetric.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Constructing the proper chain metric used in model comparison

theorem OAI.PolycyclicRecognition.exists_compact_symmetric_generating_neighborhood line 15

Source documentation

Enlarge compact generators by a compact identity neighborhood and inverses.

theorem exists_compact_symmetric_generating_neighborhood
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [LocallyCompactSpace G] {L : Set G} (hL : IsCompact L)
    (hgen : Subgroup.closure L = ⊤) :
    ∃ K : Set G, IsCompact K ∧ K ∈ 𝓝 (1 : G) ∧
      Subgroup.closure K = ⊤ ∧ ∀ g : G, g⁻¹ ∈ K ↔ g ∈ K := by
…

theorem OAI.PolycyclicRecognition.geodesicMetricExistenceInput line 36
Source documentation
Specialization of the proper chain-metric construction to the exact compact-generation input used by the recognition theorem.
```
theorem geodesicMetricExistenceInput : GeodesicMetricExistenceInput := by
…
```
Mentions: OAI.PolycyclicRecognition.GeodesicMetricExistenceInput