OAI/GroupTheory/SimpleAmenable/CentralCovers/PrimitiveTable.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.subtypeAlternatingHom_injective line 17
  2. def OAI.SimpleAmenable.tableAlphabetHom line 23
  3. theorem OAI.SimpleAmenable.tableAlphabetHom_injective line 29
  4. def OAI.SimpleAmenable.actualAlphabetTableHom line 35
  5. theorem OAI.SimpleAmenable.actualAlphabetTableHom_injective line 40
  6. def OAI.SimpleAmenable.actualTestMask line 44
  7. theorem OAI.SimpleAmenable.actualTestMask_separates line 48
  8. theorem OAI.SimpleAmenable.tableAlphabetHom_mask line 56
  9. theorem OAI.SimpleAmenable.actualPolygonTableHom_whole line 63
  10. theorem OAI.SimpleAmenable.actualAlphabetTableHom_masks line 77
  11. def OAI.SimpleAmenable.InitialCoverSystem.primitiveTests line 99
  12. theorem OAI.SimpleAmenable.InitialCoverSystem.primitiveFamily_aligned line 103
  13. def OAI.SimpleAmenable.InitialCoverSystem.primitiveTable line 115
  14. theorem OAI.SimpleAmenable.InitialCoverSystem.primitiveTable_sector_aligned line 129