OAI/SetTheory/PartitionPrinciple/Geometry/GroundFinalInsertionExceptions.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.NatUnionCode.partialOrder line 11
2. theorem OAI.PartitionPilot.Forcing.NatUnionCode.order_entry_iff line 40
3. theorem OAI.PartitionPilot.Forcing.NatUnionCode.meetOrder line 54
4. theorem OAI.PartitionPilot.Forcing.NatUnionCode.meet_entry_iff line 83
5. def OAI.PartitionPilot.Forcing.CodedInsertionProfile line 98
6. theorem OAI.PartitionPilot.Forcing.CodedInsertionProfile.iff_profile line 103
7. theorem OAI.PartitionPilot.Forcing.CodedTemplateAttachment.insertion_profile_persists line 139
8. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.insertion_profile_persists line 169
9. structure OAI.PartitionPilot.Forcing.CodedCapProfile line 186
10. def OAI.PartitionPilot.Forcing.CodedCompressionProfiles line 197
11. theorem OAI.PartitionPilot.Forcing.NatUnionCode.insertionProfile line 209
12. theorem OAI.PartitionPilot.Forcing.CodedInsertionProfile.cap_iff_positive line 241
13. theorem OAI.PartitionPilot.Forcing.CodedInsertionProfile.negative_incomparable line 257
14. theorem OAI.PartitionPilot.Forcing.CodedCapProfile.cap_iff_positive line 276
15. theorem OAI.PartitionPilot.Forcing.CodedCapProfile.negative_incomparable line 286
16. structure OAI.PartitionPilot.Forcing.FinalInsertionFamiliesCode line 305
17. theorem OAI.PartitionPilot.Forcing.FinalInsertionFamiliesCode.tests line 322
18. def OAI.PartitionPilot.Forcing.FinalInsertionFamiliesCode.decodedCaps line 345
19. def OAI.PartitionPilot.Forcing.FinalInsertionFamiliesCode.decodedActors line 351
20. theorem OAI.PartitionPilot.Forcing.FinalInsertionFamiliesCode.decodedCaps_entry line 357
21. theorem OAI.PartitionPilot.Forcing.FinalInsertionFamiliesCode.decodedActors_entry line 364
22. theorem OAI.PartitionPilot.Forcing.FinalInsertionFamiliesCode.hasInsertionFamily line 371
23. def OAI.PartitionPilot.Forcing.capExceptionTest line 409
24. def OAI.PartitionPilot.Forcing.capExceptionRelation line 413
25. theorem OAI.PartitionPilot.Forcing.pair_mem_capExceptionRelation line 419
26. def OAI.PartitionPilot.Forcing.capExceptionEntryFormula line 433
27. theorem OAI.PartitionPilot.Forcing.truth_capExceptionEntryFormula line 443
28. theorem OAI.PartitionPilot.Forcing.TransitiveGround.capExceptionRelation_mem line 461
29. theorem OAI.PartitionPilot.Forcing.TransitiveGround.partial_image_countable line 481
30. theorem OAI.PartitionPilot.Forcing.FinalInsertionFamiliesCode.exists_ground_countable_exceptions line 505