OAI/Geometry/HyperbolicGroups/WordPicture.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicObstruction.WordPictures.invLetter line 20
  2. lemma OAI.HyperbolicObstruction.WordPictures.invLetter_invLetter line 21
  3. def OAI.HyperbolicObstruction.WordPictures.SymmetricRelator line 24
  4. lemma OAI.HyperbolicObstruction.WordPictures.symmetricRelator_inv line 27
  5. structure OAI.HyperbolicObstruction.WordPictures.WordPicture line 36

    Source documentation

    Finite, genuinely genus-zero van Kampen side-pairings, with a literal outside word and enumerated indexed relator boundaries on every interior face. There is no disk-existence or isoperimetric field.

    structure WordPicture (R : Set (Word A)) (w : Word A) where
…

    Mentions: OAI.HyperbolicObstruction.WordPictures.Word

  6. lemma OAI.HyperbolicObstruction.WordPictures.WordPicture.respects line 54
  7. def OAI.HyperbolicObstruction.WordPictures.WordPicture.mirror line 57
  8. def OAI.HyperbolicObstruction.WordPictures.WordPicture.empty line 80

    Source documentation

    No faces are required to fill the empty word.

    def empty (R : Set (Word A)) : WordPicture R [] where
…

    Mentions: OAI.HyperbolicObstruction.WordPictures.Word, OAI.HyperbolicObstruction.WordPictures.WordPicture