OAI/Geometry/PeriodicTiling/OrdinaryModel.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PeriodicTilingThree.CommonModel.ordinarySymbol line 15
  2. def OAI.PeriodicTilingThree.CommonModel.ordinaryUseful line 18
  3. def OAI.PeriodicTilingThree.CommonModel.ordinaryHigh line 21
  4. def OAI.PeriodicTilingThree.CommonModel.ordinaryWord line 24
  5. theorem OAI.PeriodicTilingThree.CommonModel.ordinaryWord_allowed line 26
  6. theorem OAI.PeriodicTilingThree.CommonModel.ordinaryUseful_eq_of_lineValue_eq line 39
  7. theorem OAI.PeriodicTilingThree.CommonModel.ordinaryUseful_active_iff line 45
  8. theorem OAI.PeriodicTilingThree.CommonModel.ordinarySymbol_offset line 51
  9. theorem OAI.PeriodicTilingThree.CommonModel.ordinaryUseful_offset line 59
  10. theorem OAI.PeriodicTilingThree.CommonModel.ordinaryHigh_offset line 65
  11. theorem OAI.PeriodicTilingThree.CommonModel.ordinarySymbol_val_of_residue line 73
  12. theorem OAI.PeriodicTilingThree.CommonModel.reduce_residue line 88
  13. theorem OAI.PeriodicTilingThree.CommonModel.ordinarySymbol_firstRegion line 95
  14. theorem OAI.PeriodicTilingThree.CommonModel.ordinarySymbol_secondRegion line 105