OAI/Combinatorics/TreeEdit/CircleSeparation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.TreeEdit.TorusTree.onePositive line 9
  2. def OAI.TreeEdit.TorusTree.representative line 11
  3. lemma OAI.TreeEdit.TorusTree.representative_mem line 13
  4. lemma OAI.TreeEdit.TorusTree.representative_coe line 16
  5. def OAI.TreeEdit.TorusTree.bin line 19
  6. lemma OAI.TreeEdit.TorusTree.bin_equal_close line 23
  7. def OAI.TreeEdit.TorusTree.State line 42
  8. instance OAI.TreeEdit.TorusTree.stateAddCommGroup line 46
  9. instance OAI.TreeEdit.TorusTree.stateFintype line 51
  10. def OAI.TreeEdit.TorusTree.diagonal line 56
  11. def OAI.TreeEdit.TorusTree.Symbol line 60
  12. instance OAI.TreeEdit.TorusTree.symbolFintype line 64
  13. lemma OAI.TreeEdit.TorusTree.symbol_card line 69
  14. def OAI.TreeEdit.TorusTree.word line 74
  15. lemma OAI.TreeEdit.TorusTree.good_children_int line 80
  16. theorem OAI.TreeEdit.TorusTree.separation line 103