OAI/SetTheory/PartitionPrinciple/Geometry/GroundIntervalSelection.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.leastIntervalCandidate line 11
2. theorem OAI.PartitionPilot.Forcing.leastIntervalCandidate_unique line 17
3. theorem OAI.PartitionPilot.Forcing.leastIntervalCandidate_exists_unique line 33
4. theorem OAI.PartitionPilot.Forcing.DenseOrderCode.least_interval_exists_unique line 55
5. def OAI.PartitionPilot.Forcing.BoundedFormula.intervalCandidateFormula line 71
6. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_intervalCandidateFormula line 77
7. def OAI.PartitionPilot.Forcing.BoundedFormula.leastIntervalCandidateFormula line 84
8. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_leastIntervalCandidateFormula line 92
9. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_leastIntervalCandidateFormula line 105
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_unique_ground_intervalSelection line 117