OAI/SetTheory/PartitionPrinciple/Geometry/GroundInitialCompletedCompressionCertificates.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.SetFormula.historyFieldUnionElementFormula line 15
2. def OAI.PartitionPilot.Forcing.SetFormula.historyFieldUnionFormula line 20
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_historyFieldUnionElementFormula line 28
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_historyFieldUnionFormula line 61
5. theorem OAI.PartitionPilot.Forcing.GroundCompressionUnionData.realize_canonicalFieldUnionFormula line 83
6. def OAI.PartitionPilot.Forcing.SetFormula.historyFieldUnionTupleFormula line 102
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_historyFieldUnionTupleFormula line 113
8. def OAI.PartitionPilot.Forcing.GroundCompressionUnionData.code line 161
9. theorem OAI.PartitionPilot.Forcing.GroundCompressionUnionData.code_ground line 163
10. theorem OAI.PartitionPilot.Forcing.GroundCompressionUnionData.realize_canonicalUnionTupleFormula line 166
11. structure OAI.PartitionPilot.Forcing.GroundInitialCompressionCertificate line 183
12. def OAI.PartitionPilot.Forcing.GroundInitialCompressionCertificate.history line 205
13. def OAI.PartitionPilot.Forcing.GroundInitialCompressionCertificate.code line 209
14. theorem OAI.PartitionPilot.Forcing.GroundInitialCompressionCertificate.history_ground line 213
15. theorem OAI.PartitionPilot.Forcing.GroundInitialCompressionCertificate.code_ground line 229
16. theorem OAI.PartitionPilot.Forcing.GroundMainStage.compressionCertificate_of_representatives line 250
17. theorem OAI.PartitionPilot.Forcing.GroundMainStage.exists_compressionCertificate line 276
18. theorem OAI.PartitionPilot.Forcing.GroundInitialCompressionCertificate.realize_history_iff line 306
19. theorem OAI.PartitionPilot.Forcing.GroundInitialCompressionCertificate.realize_union_iff line 325
20. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.initial_union_range_accounting line 347
21. abbrev OAI.PartitionPilot.Forcing.GroundInitialCompressionCertificate.Completion line 419
22. theorem OAI.PartitionPilot.Forcing.GroundInitialCompressionCertificate.completion_union line 423
23. theorem OAI.PartitionPilot.Forcing.GroundInitialCompressionCertificate.exists_completion line 427
24. theorem OAI.PartitionPilot.Forcing.GroundInitialCompressionCertificate.completion_profiles line 452
25. theorem OAI.PartitionPilot.Forcing.GroundInitialCompressionCertificate.completion_original_data line 486
26. structure OAI.PartitionPilot.Forcing.GroundInitialCompletedCompressionCertificate line 512
27. def OAI.PartitionPilot.Forcing.GroundInitialCompletedCompressionCertificate.code line 523
28. theorem OAI.PartitionPilot.Forcing.GroundInitialCompletedCompressionCertificate.code_ground line 529
29. theorem OAI.PartitionPilot.Forcing.GroundInitialCompressionCertificate.exists_completedCertificate line 547