OAI/SetTheory/PartitionPrinciple/Transfinite/GroundMainPrefixFinalStrictGrowth.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.selectedStep_terminal_entry line 18
2. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.terminal_successor_entry line 48
3. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.terminal_successor_taskBearing line 68
4. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.final_rectangle_at_bound line 81
5. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.final_rectangle_at_bound_of_trace line 138
6. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPoints_separation line 172
7. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPoints_separation_of_trace line 222
8. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPoints_strict_extension line 254
9. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.terminal_adjacent_strict_top line 274
10. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPoints_strict_extension_of_trace line 300