OAI/SetTheory/PartitionPrinciple/Definability/BatchAttachmentRealization.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PartitionPilot.Forcing.CodedTemplateAttachment line 11
2. abbrev OAI.PartitionPilot.Forcing.CodedTemplateAttachment.Nodes line 28
3. def OAI.PartitionPilot.Forcing.CodedTemplateAttachment.encode line 30
4. abbrev OAI.PartitionPilot.Forcing.CodedTemplateAttachment.carrier line 34
5. abbrev OAI.PartitionPilot.Forcing.CodedTemplateAttachment.order line 35
6. abbrev OAI.PartitionPilot.Forcing.CodedTemplateAttachment.meetGraph line 37
7. theorem OAI.PartitionPilot.Forcing.CodedTemplateAttachment.encode_mem line 39
8. theorem OAI.PartitionPilot.Forcing.CodedTemplateAttachment.encode_injective line 44
9. theorem OAI.PartitionPilot.Forcing.CodedTemplateAttachment.encode_surjective line 60
10. theorem OAI.PartitionPilot.Forcing.CodedTemplateAttachment.fresh_le_iff line 68
11. theorem OAI.PartitionPilot.Forcing.CodedTemplateAttachment.le_encode line 81
12. theorem OAI.PartitionPilot.Forcing.CodedTemplateAttachment.partialOrder line 157
13. theorem OAI.PartitionPilot.Forcing.CodedTemplateAttachment.encoded_meet_glb line 174
14. theorem OAI.PartitionPilot.Forcing.CodedTemplateAttachment.meetOrder line 184
15. theorem OAI.PartitionPilot.Forcing.CodedTemplateAttachment.encoded_meet_entry line 191
16. def OAI.PartitionPilot.Forcing.batchAttachmentInsideGraph line 207
17. def OAI.PartitionPilot.Forcing.batchAttachmentUpperGraph line 214
18. theorem OAI.PartitionPilot.Forcing.batchAttachmentInsideGraph_subset line 221
19. theorem OAI.PartitionPilot.Forcing.batchAttachmentUpperGraph_subset line 226
20. theorem OAI.PartitionPilot.Forcing.mem_batchAttachmentInsideGraph line 230
21. theorem OAI.PartitionPilot.Forcing.mem_batchAttachmentUpperGraph line 245
22. theorem OAI.PartitionPilot.Forcing.pair_mem_batchAttachmentInsideGraph line 259
23. theorem OAI.PartitionPilot.Forcing.pair_mem_batchAttachmentUpperGraph line 275
24. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.inside_entry_iff line 294
25. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.upper_entry_iff line 306
26. def OAI.PartitionPilot.Forcing.AttachmentBatchInputs.freshCode line 330
27. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.freshCode_mem line 333
28. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.freshCode_injective line 339
29. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.freshCode_surjective line 346
30. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.freshCode_shadow_entry line 357
31. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.freshCode_shadow_value line 363
32. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.freshCode_inside_iff line 370
33. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.freshCode_upper_iff line 386
34. def OAI.PartitionPilot.Forcing.AttachmentBatchInputs.coding line 394
35. abbrev OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batchCarrier line 407
36. abbrev OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batchOrder line 408
37. abbrev OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batchMeetGraph line 409
38. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batch_meetOrder line 411
39. def OAI.PartitionPilot.Forcing.BoundedFormula.pairOfPairsFormula line 425
40. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_pairOfPairsFormula line 431
41. def OAI.PartitionPilot.Forcing.BoundedFormula.batchAttachmentInsideEntryFormula line 449
42. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_batchAttachmentInsideEntryFormula line 456
43. def OAI.PartitionPilot.Forcing.BoundedFormula.batchAttachmentUpperEntryFormula line 466
44. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_batchAttachmentUpperEntryFormula line 473
45. theorem OAI.PartitionPilot.Forcing.TransitiveGround.batchAttachmentInsideGraph_mem line 490
46. theorem OAI.PartitionPilot.Forcing.TransitiveGround.batchAttachmentUpperGraph_mem line 516