OAI/Geometry/PeriodicTiling/ChannelDigitBlocks.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PeriodicTilingThree.ChannelOtherDigits line 14
  2. abbrev OAI.PeriodicTilingThree.ChannelBlockA line 17
  3. abbrev OAI.PeriodicTilingThree.ChannelBlockB line 20
  4. def OAI.PeriodicTilingThree.channelDigitBase line 23
  5. def OAI.PeriodicTilingThree.channelDigitBlocks line 29
  6. theorem OAI.PeriodicTilingThree.channelDigitBlocks_C line 35
  7. theorem OAI.PeriodicTilingThree.channelDigitBlocks_C_eq line 41
  8. theorem OAI.PeriodicTilingThree.channelDigitBlocks_active_iff line 46
  9. def OAI.PeriodicTilingThree.LabeledBlocks.castSizes line 70
  10. theorem OAI.PeriodicTilingThree.LabeledBlocks.T_transport_apply line 77
  11. theorem OAI.PeriodicTilingThree.LabeledBlocks.T_onCoordinate line 81
  12. theorem OAI.PeriodicTilingThree.LabeledBlocks.T_onCoordinate_other line 88
  13. theorem OAI.PeriodicTilingThree.LabeledBlocks.T_onCoordinate_transport_other line 95
  14. theorem OAI.PeriodicTilingThree.channelDigitBlocks_T_other line 105
  15. def OAI.PeriodicTilingThree.seedOneBlocks line 113
  16. def OAI.PeriodicTilingThree.seedTwoBlocks line 120