WordPictureBase.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.PictureSwitch.finRange_boundary line 16
def OAI.HyperbolicObstruction.WordPictures.WordPicture.polygon line 39
Source documentation
The two sides of a genuine relator disk and its distinguished exterior. Every side is separately indexed, even when its letter is repeated.
```
def polygon (hw : w ∈ R) (hne : w ≠ []) : WordPicture R w where
…
```
Mentions: OAI.HyperbolicObstruction.WordPictures.WordPicture
lemma OAI.HyperbolicObstruction.WordPictures.WordPicture.of_relator line 73
def OAI.HyperbolicObstruction.WordPictures.WordPicture.freePair line 80
Source documentation
A freely canceling pair is the boundary of a single thickened edge, with no interior cell.
```
def freePair (R : Set (Word A)) (a : A × Bool) : WordPicture R [a,invLetter a] where
…
```
Mentions: OAI.HyperbolicObstruction.WordPictures.Word, OAI.HyperbolicObstruction.WordPictures.WordPicture, OAI.HyperbolicObstruction.WordPictures.invLetter