OAI/Analysis/FreeGroupFactor/InfiniteGeneration.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FreeGroupFactorMain.Generation.norm_comp_sub_le line 16
  2. theorem OAI.FreeGroupFactorMain.Generation.twoNorm_comp_sub_le line 23
  3. theorem OAI.FreeGroupFactorMain.Generation.twoNorm_map_sub_fixed line 32
  4. theorem OAI.FreeGroupFactorMain.Generation.mapTuple_dist_lt line 41
  5. theorem OAI.FreeGroupFactorMain.Generation.conjugate_fix line 50
  6. theorem OAI.FreeGroupFactorMain.Generation.conjugate_norm_sub line 55
  7. theorem OAI.FreeGroupFactorMain.Generation.conjugate_twoNorm_sub line 60
  8. abbrev OAI.FreeGroupFactorMain.InfiniteGeneration.Index line 72
  9. abbrev OAI.FreeGroupFactorMain.InfiniteGeneration.Group line 73
  10. abbrev OAI.FreeGroupFactorMain.InfiniteGeneration.M line 74
  11. abbrev OAI.FreeGroupFactorMain.InfiniteGeneration.Tuple line 75
  12. def OAI.FreeGroupFactorMain.InfiniteGeneration.initial line 77
  13. def OAI.FreeGroupFactorMain.InfiniteGeneration.extra line 78
  14. theorem OAI.FreeGroupFactorMain.InfiniteGeneration.word_initial line 81
  15. theorem OAI.FreeGroupFactorMain.InfiniteGeneration.permutation_iso line 91
  16. theorem OAI.FreeGroupFactorMain.InfiniteGeneration.swapped_extra_iso line 102
  17. theorem OAI.FreeGroupFactorMain.InfiniteGeneration.one_step_extra_of_none line 128
  18. theorem OAI.FreeGroupFactorMain.Generation.word_twoNorm_finite_bound line 178
  19. theorem OAI.FreeGroupFactorMain.Generation.poly_twoNorm_finite_bound line 211
  20. theorem OAI.FreeGroupFactorMain.InfiniteGeneration.finite_word_continuity line 248
  21. theorem OAI.FreeGroupFactorMain.InfiniteGeneration.finite_absorption line 260
  22. def OAI.FreeGroupFactorMain.InfiniteGeneration.orbit line 319
  23. theorem OAI.FreeGroupFactorMain.InfiniteGeneration.orbit_nonempty line 322
  24. def OAI.FreeGroupFactorMain.InfiniteGeneration.extraLabel line 327
  25. def OAI.FreeGroupFactorMain.InfiniteGeneration.replacement line 328
  26. theorem OAI.FreeGroupFactorMain.InfiniteGeneration.orbit_step line 331
  27. theorem OAI.FreeGroupFactorMain.InfiniteGeneration.orbit_local_approximation line 379
  28. theorem OAI.FreeGroupFactorMain.InfiniteGeneration.orbit_trace line 410
  29. theorem OAI.FreeGroupFactorMain.InfiniteGeneration.closure_orbit_trace line 422
  30. theorem OAI.FreeGroupFactorMain.InfiniteGeneration.generating_haar_tuple line 431