OAI/SetTheory/PartitionPrinciple/Geometry/BinaryTiles.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input line 13
2. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.Fresh line 22
3. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.Node line 24
4. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.shadow line 26
5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.shadow_le_anchor line 28
6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.shadow_mono line 31
7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.shadow_meet line 34
8. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.data line 39
9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.component_meets line 56
10. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.order line 64
11. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.left line 66
12. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.represent line 68
13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.represent_old line 73
14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.represent_new line 78
15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.represent_le_iff line 83
16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.old_below_represent line 103
17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.represented_meet line 114
18. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.right line 130
19. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.cover line 135
20. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.left_ideal line 140
21. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.overlap_exact line 146
22. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.old_in_right line 161
23. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.right_ideal line 172
24. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.cross_meet line 180
25. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.new_shadow_meet line 188
26. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.principal_cross_meet line 192
27. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.greatest_old_part line 205
28. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.left_principal line 209
29. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.right_principal line 216
30. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.least_preserved line 223
31. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.bottoms_agree line 230
32. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalAmalgamation.Input.comparison_in_vertex line 240
33. def OAI.PartitionPilot.Compression.RecursiveMaps.BinaryTiles.vertex line 263
34. theorem OAI.PartitionPilot.Compression.RecursiveMaps.BinaryTiles.vertex_cover line 267
35. def OAI.PartitionPilot.Compression.RecursiveMaps.BinaryTiles.separation line 273
36. theorem OAI.PartitionPilot.Compression.RecursiveMaps.BinaryTiles.separation_fixes line 284
37. theorem OAI.PartitionPilot.Compression.RecursiveMaps.BinaryTiles.separation_intersection line 288
38. theorem OAI.PartitionPilot.Compression.RecursiveMaps.BinaryTiles.separation_cross_meet line 292
39. def OAI.PartitionPilot.Compression.RecursiveMaps.BinaryTiles.compression line 303
40. theorem OAI.PartitionPilot.Compression.RecursiveMaps.BinaryTiles.compression_identification line 315
41. theorem OAI.PartitionPilot.Compression.RecursiveMaps.BinaryTiles.compression_no_new_nodes line 321
42. theorem OAI.PartitionPilot.Compression.RecursiveMaps.BinaryTiles.compression_top line 328