OAI/Analysis/LipschitzFree/FiniteQuotients.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Finite permutation representations of balls in free groups

  1. def OAI.DiscreteFree.GraphProducer.WordBall line 16
  2. instance OAI.DiscreteFree.GraphProducer.(instance at line 18) line 18
  3. instance OAI.DiscreteFree.GraphProducer.(instance at line 28) line 28
  4. def OAI.DiscreteFree.GraphProducer.ballOne line 30
  5. theorem OAI.DiscreteFree.GraphProducer.ballOne_val line 33
  6. theorem OAI.DiscreteFree.GraphProducer.exists_ball_perm line 35
  7. def OAI.DiscreteFree.GraphProducer.ballPerm line 52
  8. theorem OAI.DiscreteFree.GraphProducer.ballPerm_apply line 55
  9. theorem OAI.DiscreteFree.GraphProducer.ballPerm_inv_apply line 60
  10. def OAI.DiscreteFree.GraphProducer.ballRep line 72
  11. lemma OAI.DiscreteFree.GraphProducer.mk_cons_letter line 76
  12. theorem OAI.DiscreteFree.GraphProducer.ballRep_word line 81
  13. theorem OAI.DiscreteFree.GraphProducer.ballRep_apply_one line 110
  14. theorem OAI.DiscreteFree.GraphProducer.ballRep_injective_on line 114
  15. theorem OAI.DiscreteFree.GraphProducer.ballRep_ne_one line 120
  16. theorem OAI.DiscreteFree.GraphProducer.prefixes_injective line 130