OAI/SetTheory/PartitionPrinciple/Geometry/GroundSingleAttachment.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PartitionPilot.Forcing.SingleAttachmentInputs line 11
2. abbrev OAI.PartitionPilot.Forcing.SingleAttachmentInputs.Base line 32
3. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.base_mem line 35
4. def OAI.PartitionPilot.Forcing.SingleAttachmentInputs.baseMap line 38
5. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.baseMap_entry line 43
6. def OAI.PartitionPilot.Forcing.SingleAttachmentInputs.baseEmbedding line 46
7. def OAI.PartitionPilot.Forcing.SingleAttachmentInputs.templates line 64
8. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.shadow_entry line 85
9. structure OAI.PartitionPilot.Forcing.AttachmentBatchInputs line 102
10. abbrev OAI.PartitionPilot.Forcing.AttachmentBatchInputs.space line 122
11. abbrev OAI.PartitionPilot.Forcing.AttachmentBatchInputs.rel line 123
12. abbrev OAI.PartitionPilot.Forcing.AttachmentBatchInputs.meet line 124
13. abbrev OAI.PartitionPilot.Forcing.AttachmentBatchInputs.anchor line 125
14. abbrev OAI.PartitionPilot.Forcing.AttachmentBatchInputs.embed line 126
15. abbrev OAI.PartitionPilot.Forcing.AttachmentBatchInputs.filter line 127
16. abbrev OAI.PartitionPilot.Forcing.AttachmentBatchInputs.separator line 128
17. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.space_entry line 130
18. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.rel_entry line 133
19. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.meet_entry line 136
20. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.anchor_entry line 139
21. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.embed_entry line 142
22. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.filter_entry line 145
23. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.separator_entry line 148
24. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.fiber line 151
25. def OAI.PartitionPilot.Forcing.AttachmentBatchInputs.templates line 157
26. abbrev OAI.PartitionPilot.Forcing.SingleAttachmentInputs.Nodes line 191
27. def OAI.PartitionPilot.Forcing.SingleAttachmentInputs.encode line 193
28. abbrev OAI.PartitionPilot.Forcing.SingleAttachmentInputs.carrier line 197
29. abbrev OAI.PartitionPilot.Forcing.SingleAttachmentInputs.order line 198
30. abbrev OAI.PartitionPilot.Forcing.SingleAttachmentInputs.meetGraph line 200
31. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.fresh_mem line 202
32. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.encode_mem line 205
33. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.encode_injective line 210
34. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.encode_surjective line 232
35. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.fresh_lower_iff line 239
36. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.le_encode line 255
37. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.partialOrder line 329
38. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.encoded_meet_glb line 346
39. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.meetOrder line 356
40. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.encoded_meet_entry line 363
41. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.pushforward line 377
42. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.base_injection line 428
43. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.template_graph_entry line 438
44. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.template_graph_entry_iff line 451
45. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.encoded_embedding_order_iff line 461
46. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.encoded_embedding_code line 478
47. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.old_embedding_code line 511
48. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.template_embedding_code line 518
49. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.old_order_iff line 524
50. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.template_order_iff line 532
51. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.template_old_agreement line 539
52. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.template_shadow_entry line 546
53. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.old_below_template_iff line 557
54. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.fresh_old_upper_iff line 584
55. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.fresh_old_meet_code line 590
56. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.greatest_preserved line 617
57. theorem OAI.PartitionPilot.Forcing.SingleAttachmentInputs.least_preserved line 625
58. theorem OAI.PartitionPilot.Forcing.TransitiveGround.singleAttachment_ground_codes line 643
59. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_singleAttachment line 665