OAI/GroupTheory/SimpleAmenable/CentralCovers/FullSector.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.InitialCoverSystem.fullGeometricSector_supported line 22
  2. theorem OAI.SimpleAmenable.InitialCoverSystem.constant_small_supported line 35
  3. theorem OAI.SimpleAmenable.InitialCoverSystem.fullGeometricSector_small_control line 43
  4. theorem OAI.SimpleAmenable.InitialCoverSystem.fullGeometricSector_commute line 51
  5. theorem OAI.SimpleAmenable.universal_five_alphabet_hom_ext line 69
  6. theorem OAI.SimpleAmenable.InitialCoverSystem.fullGeometricSector_subfamily line 87
  7. def OAI.SimpleAmenable.InitialCoverSystem.windowSector line 109
  8. theorem OAI.SimpleAmenable.InitialCoverSystem.windowSector_inclusion line 115
  9. theorem OAI.SimpleAmenable.InitialCoverSystem.windowSector_overlap_control line 125
  10. def OAI.SimpleAmenable.axisWindowPrimitives line 145
  11. theorem OAI.SimpleAmenable.axisInterval_resolved line 149
  12. def OAI.SimpleAmenable.axisWindowEmbedding line 203
  13. theorem OAI.SimpleAmenable.axisWindowEmbedding_spec line 210
  14. theorem OAI.SimpleAmenable.InitialCoverSystem.axisFamilyLaw line 230
  15. def OAI.SimpleAmenable.InitialCoverSystem.axisSector line 236
  16. theorem OAI.SimpleAmenable.InitialCoverSystem.axisSector_in_window line 243
  17. theorem OAI.SimpleAmenable.InitialCoverSystem.axisSector_overlap_control line 252