OAI/GroupTheory/SimpleAmenable/PolygonGeometry/SectorControl.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.ActualLawfulTable.sector_control line 20
  2. theorem OAI.SimpleAmenable.resolvedPolygonMask_univ line 37
  3. theorem OAI.SimpleAmenable.InitialCoverSystem.geometricSector_whole line 47
  4. theorem OAI.SimpleAmenable.InitialCoverSystem.geometricSector_control line 68
  5. theorem OAI.SimpleAmenable.InitialCoverSystem.geometricSector_input line 82
  6. theorem OAI.SimpleAmenable.subtypeAlternatingHom_mem_range line 107
  7. def OAI.SimpleAmenable.subalphabetHom line 119
  8. theorem OAI.SimpleAmenable.subtypeAlternatingHom_comp line 126
  9. def OAI.SimpleAmenable.CommonFrame.restrict line 136
  10. theorem OAI.SimpleAmenable.InitialCoverSystem.initialAlphabet_inclusion line 149
  11. theorem OAI.SimpleAmenable.InitialCoverSystem.primitiveCopy_inclusion line 154
  12. theorem OAI.SimpleAmenable.InitialCoverSystem.primitiveFamily_inclusion line 163
  13. theorem OAI.SimpleAmenable.InitialCoverSystem.primitiveFamily_range_inclusion line 171
  14. theorem OAI.SimpleAmenable.InitialCoverSystem.geometricSector_inclusion line 183