OAI/SetTheory/PartitionPrinciple/Definability/IntervalSequenceFormulas.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PartitionPilot.Forcing.IntervalSequenceCode line 11
2. def OAI.PartitionPilot.Forcing.intervalNextCandidate line 20
3. theorem OAI.PartitionPilot.Forcing.pair_mem_intervalSequenceInsert line 27
4. theorem OAI.PartitionPilot.Forcing.IntervalSequenceCode.empty line 34
5. theorem OAI.PartitionPilot.Forcing.IntervalSequenceCode.restrict line 43
6. theorem OAI.PartitionPilot.Forcing.IntervalSequenceCode.insert line 60
7. def OAI.PartitionPilot.Forcing.leastIntervalNextCandidate line 130
8. theorem OAI.PartitionPilot.Forcing.leastIntervalNextCandidate_unique line 136
9. theorem OAI.PartitionPilot.Forcing.leastIntervalNextCandidate_exists_unique line 152
10. def OAI.PartitionPilot.Forcing.BoundedFormula.iffFormula line 178
11. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_iffFormula line 181
12. def OAI.PartitionPilot.Forcing.BoundedFormula.intervalNextCandidateFormula line 186
13. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_intervalNextCandidateFormula line 200
14. def OAI.PartitionPilot.Forcing.BoundedFormula.leastIntervalNextCandidateFormula line 209
15. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_leastIntervalNextCandidateFormula line 217
16. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_leastIntervalNextCandidateFormula line 232
17. def OAI.PartitionPilot.Forcing.SetFormula.intervalSequenceStepFormula line 245
18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_intervalSequenceStepFormula line 254
19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_unique_ground_intervalNext line 263