OAI/Geometry/PeriodicTiling/LabeledDigitBlocks.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PeriodicTilingThree.LabeledBlocks line 12
  2. def OAI.PeriodicTilingThree.LabeledBlocks.labelRotation line 19
  3. def OAI.PeriodicTilingThree.LabeledBlocks.C line 29
  4. def OAI.PeriodicTilingThree.LabeledBlocks.T line 34
  5. def OAI.PeriodicTilingThree.LabeledBlocks.blockId line 37
  6. def OAI.PeriodicTilingThree.LabeledBlocks.block line 42
  7. theorem OAI.PeriodicTilingThree.LabeledBlocks.unique_block line 45
  8. def OAI.PeriodicTilingThree.LabeledBlocks.blockEquivA line 49
  9. def OAI.PeriodicTilingThree.LabeledBlocks.blockEquivB line 69
  10. theorem OAI.PeriodicTilingThree.LabeledBlocks.C_decode_symm_inl line 89
  11. theorem OAI.PeriodicTilingThree.LabeledBlocks.C_decode_symm_inr line 93
  12. theorem OAI.PeriodicTilingThree.LabeledBlocks.decode_T line 97
  13. theorem OAI.PeriodicTilingThree.LabeledBlocks.T_decode_symm_inl line 101
  14. theorem OAI.PeriodicTilingThree.LabeledBlocks.T_decode_symm_inr line 107
  15. theorem OAI.PeriodicTilingThree.LabeledBlocks.blockId_T line 113
  16. theorem OAI.PeriodicTilingThree.LabeledBlocks.T_zero line 119
  17. theorem OAI.PeriodicTilingThree.LabeledBlocks.T_add line 126
  18. theorem OAI.PeriodicTilingThree.LabeledBlocks.T_neg_T line 134
  19. theorem OAI.PeriodicTilingThree.LabeledBlocks.T_T_neg line 139
  20. def OAI.PeriodicTilingThree.LabeledBlocks.transport line 144
  21. theorem OAI.PeriodicTilingThree.LabeledBlocks.C_transport line 147
  22. def OAI.PeriodicTilingThree.LabeledBlocks.copyRight line 150
  23. theorem OAI.PeriodicTilingThree.LabeledBlocks.C_copyRight line 167
  24. theorem OAI.PeriodicTilingThree.LabeledBlocks.T_copyRight line 172
  25. def OAI.PeriodicTilingThree.LabeledBlocks.digit line 179
  26. theorem OAI.PeriodicTilingThree.LabeledBlocks.C_nonconstant line 185
  27. def OAI.PeriodicTilingThree.LabeledBlocks.onCoordinate line 206
  28. theorem OAI.PeriodicTilingThree.LabeledBlocks.C_onCoordinate line 212
  29. theorem OAI.PeriodicTilingThree.LabeledBlocks.C_eq_of_coordinate_eq line 216
  30. theorem OAI.PeriodicTilingThree.LabeledBlocks.C_designated_witness line 221
  31. theorem OAI.PeriodicTilingThree.LabeledBlocks.C_active_iff line 233