OAI/GroupTheory/UniversalGroup/MarkerMachine.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Higman.FreeBasis.erase line 12
  2. theorem OAI.Higman.FreeBasis.erase_of line 17
  3. abbrev OAI.Higman.FreeBasis.span line 22
  4. theorem OAI.Higman.FreeBasis.erase_eq_self_iff line 24
  5. theorem OAI.Higman.FreeBasis.erase_comp line 45
  6. theorem OAI.Higman.FreeBasis.span_inter line 51
  7. theorem OAI.Higman.FreeBasis.of_mem_span_iff line 61
  8. theorem OAI.Higman.FreeBasis.map_span_inf line 76
  9. theorem OAI.Higman.DecoratedMarker.eq_inclusion_of_right_eq_one line 102
  10. theorem OAI.Higman.MarkerEmbedding.test_embedding line 120
  11. theorem OAI.Higman.MarkerEmbedding.embedding_inclusion line 128
  12. theorem OAI.Higman.MarkerEmbedding.kernel_intersection line 135
  13. lemma OAI.Higman.MarkerEmbedding.projection_kernelMap line 157
  14. lemma OAI.Higman.MarkerEmbedding.range_projection_support line 168
  15. lemma OAI.Higman.MarkerEmbedding.decorated_letter_mem_range line 178
  16. theorem OAI.Higman.MarkerEmbedding.decorated_kernel_intersection line 185
  17. def OAI.Higman.MarkerEmbedding.decoratedSubgroup line 193
  18. theorem OAI.Higman.MarkerEmbedding.decorated_intersection line 196
  19. theorem OAI.Higman.MarkerEmbedding.decoratedSubgroup_eq_closure line 204
  20. def OAI.Higman.MarkerEmbedding.pullDecoration line 216
  21. lemma OAI.Higman.MarkerEmbedding.embedding_decorated line 219
  22. lemma OAI.Higman.MarkerEmbedding.map_decoratedSubgroup line 226
  23. theorem OAI.Higman.MarkerEmbedding.comap_decoratedSubgroup line 233
  24. def OAI.Higman.PartialIso.ofEmbeddings line 247
  25. theorem OAI.Higman.PartialIso.ofEmbeddings_apply line 253
  26. lemma OAI.Higman.PartialIso.ofEmbeddings_invariant_iff line 259
  27. structure OAI.Higman.MarkerMachine.Edge line 277
  28. def OAI.Higman.MarkerMachine.Edge.input line 296
  29. def OAI.Higman.MarkerMachine.Edge.output line 297
  30. def OAI.Higman.MarkerMachine.Edge.inputMap line 299
  31. def OAI.Higman.MarkerMachine.Edge.outputMap line 301
  32. lemma OAI.Higman.MarkerMachine.Edge.input_index_injective line 304
  33. lemma OAI.Higman.MarkerMachine.Edge.output_index_injective line 307
  34. lemma OAI.Higman.MarkerMachine.Edge.inputMap_injective line 311
  35. lemma OAI.Higman.MarkerMachine.Edge.outputMap_injective line 313
  36. def OAI.Higman.MarkerMachine.Edge.partialIso line 316
  37. lemma OAI.Higman.MarkerMachine.Edge.inputMap_decorated line 319
  38. lemma OAI.Higman.MarkerMachine.Edge.outputMap_decorated line 324
  39. lemma OAI.Higman.MarkerEmbedding.decoratedSubgroup_congr line 336
  40. theorem OAI.Higman.MarkerMachine.Edge.invariant line 349
  41. lemma OAI.Higman.MarkerMachine.Edge.invariant_decorated_iff line 369
  42. lemma OAI.Higman.MarkerMachine.Edge.source_fg line 380
  43. inductive OAI.Higman.MarkerMachine.Reach line 393
  44. lemma OAI.Higman.MarkerMachine.reach_iff line 400
  45. def OAI.Higman.MarkerMachine.word line 404
  46. theorem OAI.Higman.MarkerMachine.orbit_eq line 407
  47. theorem OAI.Higman.MarkerMachine.benign line 439