Model.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Release075.TorsionFree line 10
Source documentation
No nonidentity element has finite order. This does not assert unique roots.
Also declared: ComparatorChallenges/TorsionFreeHyperbolic.lean:10 (same declaration text).
```
def TorsionFree (G : Type u) [Group G] : Prop :=
…
```
def OAI.Release075.Geodesic line 14
Source documentation
A shortest edge path in the unit-edge graph.
Also declared: ComparatorChallenges/TorsionFreeHyperbolic.lean:14 (same declaration text).
```
def Geodesic {V : Type u} (X : SimpleGraph V) {x y : V} (p : X.Walk x y) : Prop :=
…
```
def OAI.Release075.SideThin line 18
Source documentation
Each vertex of p is within δ of a vertex of q or r.
Also declared: ComparatorChallenges/TorsionFreeHyperbolic.lean:18 (same declaration text).
```
def SideThin {V : Type u} (X : SimpleGraph V) (δ : ℕ) {x y z : V}
    (p : X.Walk x y) (q : X.Walk y z) (r : X.Walk z x) : Prop :=
…
```
def OAI.Release075.WordHyperbolic line 24
Source documentation
A finitely generated group with a unit-edge Cayley graph whose geodesic triangles are uniformly thin. Connectedness of this Cayley graph asserts that S generates.
Also declared: ComparatorChallenges/TorsionFreeHyperbolic.lean:24 (same declaration text).
```
def WordHyperbolic (G : Type u) [Group G] : Prop :=
…
```