OAI/Geometry/PeriodicTiling/FiniteMasks.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PeriodicTilingThree.tileIndicator line 19
  2. theorem OAI.PeriodicTilingThree.tileIndicator_nonneg line 22
  3. theorem OAI.PeriodicTilingThree.tileIndicator_le_one line 28
  4. theorem OAI.PeriodicTilingThree.tileIndicator_nat_le_one line 34
  5. theorem OAI.PeriodicTilingThree.sum_tileIndicator_cast line 40
  6. def OAI.PeriodicTilingThree.tileCount line 54
  7. theorem OAI.PeriodicTilingThree.tileCount_eq_card_filter line 57
  8. theorem OAI.PeriodicTilingThree.tileCount_le_card line 62
  9. theorem OAI.PeriodicTilingThree.tileCount_cast line 68
  10. theorem OAI.PeriodicTilingThree.tiles_iff_tileCount_eq_one line 73
  11. theorem OAI.PeriodicTilingThree.Tiles.tileCount_eq_one line 103
  12. theorem OAI.PeriodicTilingThree.Tiles.sum_tileIndicator_eq_one line 107
  13. def OAI.PeriodicTilingThree.maskAction line 118
  14. theorem OAI.PeriodicTilingThree.maskAction_zero line 121
  15. theorem OAI.PeriodicTilingThree.maskAction_single line 125
  16. theorem OAI.PeriodicTilingThree.maskAction_add line 129
  17. theorem OAI.PeriodicTilingThree.maskAction_sum line 136
  18. theorem OAI.PeriodicTilingThree.maskAction_single_mul line 144
  19. theorem OAI.PeriodicTilingThree.maskAction_mul line 155
  20. theorem OAI.PeriodicTilingThree.maskAction_one line 163
  21. theorem OAI.PeriodicTilingThree.maskAction_translate line 168
  22. def OAI.PeriodicTilingThree.familyMask line 176
  23. def OAI.PeriodicTilingThree.tileMask line 180
  24. theorem OAI.PeriodicTilingThree.maskAction_familyMask line 183
  25. theorem OAI.PeriodicTilingThree.maskAction_tileMask line 188
  26. theorem OAI.PeriodicTilingThree.maskAction_familyMask_const line 192
  27. theorem OAI.PeriodicTilingThree.maskAction_familyMask_pow_const line 197
  28. theorem OAI.PeriodicTilingThree.maskAction_familyMask_pow_succ line 207