Selection.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.HyperbolicObstruction.CATActionWitness line 16
Source documentation
A genuine action on an arbitrary chosen space in the specified universe.
```
structure CATActionWitness (G : Type a) [Group G] where
…
```
lemma OAI.HyperbolicObstruction.catActionWitness_iff line 28
theorem OAI.HyperbolicObstruction.SamplingSequence.reindex line 45
theorem OAI.HyperbolicObstruction.MasterGraph.exists_noAction line 84
Source documentation
The geometric half of selection: any infinite-group sequence with the literal sampling assertions and six-letter rows has a no-action member.
```
theorem exists_noAction : ∃ n, NoGeometricCATZeroAction.{b} (G n) := by
…
```
theorem OAI.HyperbolicObstruction.MasterGraph.eventually_noAction line 100
Source documentation
Eventually the groups admit no geometric CAT(0) action.
```
theorem eventually_noAction : ∀ᶠ n in atTop, NoGeometricCATZeroAction.{b} (G n) := by
…
```