OAI/SetTheory/PartitionPrinciple/Geometry/RectangleTile.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Vertex line 11
  2. instance OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.(instance at line 15) line 15
  3. structure OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input line 21
  4. def OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.W line 38
  5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.agree_W line 40
  6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.root_intersection line 42
  7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.image_bound line 54
  8. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.g1_bound line 67
  9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.g2_bound line 71
  10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.inverse1_C line 77
  11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.inverse2_C line 82
  12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.root_domain1 line 87
  13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.root_domain2 line 93
  14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.inverses_agree line 99
  15. def OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.anchor line 109
  16. def OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.transition line 120
  17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.triangle_domain line 127
  18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.triangle_change line 138
  19. def OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.copies line 151
  20. def OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.root line 198
  21. def OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.first line 199
  22. def OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.second line 200
  23. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.first_agrees line 202
  24. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.second_agrees line 206
  25. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.children_agree line 210
  26. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.first_root_intersection line 214
  27. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.second_root_intersection line 218
  28. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.children_intersection line 222
  29. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.meet_D_C line 226
  30. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.meet_D_B line 229
  31. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.first_root_part line 232
  32. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.second_root_part line 236
  33. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.first_meet_root line 240
  34. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.second_meet_root line 250
  35. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.children_meet line 260
  36. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.children_meet_both line 268
  37. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.three_vertex_cover line 273
  38. def OAI.PartitionPilot.Compression.RecursiveMaps.Rectangle.Input.incoming_layer line 278