OAI/Geometry/PeriodicTiling/StackingContributions.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PeriodicTilingThree.IsColorPartition line 19
  2. def OAI.PeriodicTilingThree.HasFullDifferences line 22
  3. def OAI.PeriodicTilingThree.stack line 25
  4. theorem OAI.PeriodicTilingThree.mem_stack line 30
  5. theorem OAI.PeriodicTilingThree.stack_nonempty line 35
  6. theorem OAI.PeriodicTilingThree.IsColorPartition.eq_of_mem line 43
  7. theorem OAI.PeriodicTilingThree.HasFullDifferences.nonempty line 50
  8. theorem OAI.PeriodicTilingThree.card_stack line 57
  9. theorem OAI.PeriodicTilingThree.IsColorPartition.sum_card line 71
  10. def OAI.PeriodicTilingThree.stackContributions line 97
  11. theorem OAI.PeriodicTilingThree.mem_stackContributions line 102
  12. theorem OAI.PeriodicTilingThree.stackContributions_eq_of_mem line 111
  13. theorem OAI.PeriodicTilingThree.stackContributions_card_le_one line 139
  14. theorem OAI.PeriodicTilingThree.stack_projection_injective line 146
  15. def OAI.PeriodicTilingThree.StackFiber line 163
  16. def OAI.PeriodicTilingThree.stackFiberSum line 167
  17. theorem OAI.PeriodicTilingThree.stackFiberSum_bijective line 171
  18. theorem OAI.PeriodicTilingThree.stackContributions_sum_card line 220
  19. theorem OAI.PeriodicTilingThree.stackContributions_card_eq_one line 231
  20. theorem OAI.PeriodicTilingThree.tiles_of_tiles_stack line 251