OAI/Geometry/HyperbolicGroups/IndexedDiskUniqueness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Disk-chain uniqueness follows from actual genus-zero sphere vanishing. All operations retain the originally chosen precise interior cell identities.

  1. lemma OAI.HyperbolicObstruction.WordPictures.WordPicture.Indexing.chain_unique line 20
  2. lemma OAI.HyperbolicObstruction.WordPictures.WordPicture.Indexing.chain_free_eq line 45