OAI/SetTheory/PartitionPrinciple/Geometry/GroundInitialCompressionOrigin.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.heightCandidateStates line 14
2. theorem OAI.PartitionPilot.Forcing.heightCandidateStates_subset line 23
3. theorem OAI.PartitionPilot.Forcing.mem_heightCandidateStates line 27
4. theorem OAI.PartitionPilot.Forcing.pair_mem_heightCandidateStates line 42
5. def OAI.PartitionPilot.Forcing.BoundedFormula.heightCandidateEntryFormula line 69
6. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_heightCandidateEntryFormula line 80
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.heightCandidateStates_mem line 107
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.initialCompressionData_template_constancy line 147
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.initialCompressionData_iterate_template_constancy line 151
10. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.exists_groundHeightFamily line 174
11. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.exists_groundHeightData line 282
12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundInitialHeightedCompression line 354
13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundInitialProfiledCompression line 408
14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundInitialBornCompression line 466
15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundInitialCompressionOrigin line 535