OAI/SetTheory/PartitionPrinciple/Geometry/GroundMainFinalRowTerms.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundOmegaOne_member_countable line 18
2. theorem OAI.PartitionPilot.Forcing.GroundStandardInaccessible.groundOmegaOne_mem line 29
3. theorem OAI.PartitionPilot.Forcing.GroundStandardInaccessible.groundOmegaOne_rank_lt line 34
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rowPositionSequences_below line 50
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_infiniteGroundCardinal_bound line 61
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_smallRowPositionSequences line 108
7. structure OAI.PartitionPilot.Forcing.GroundMainFinalInclusions line 137
8. def OAI.PartitionPilot.Forcing.GroundMainPrefix.finalInclusions line 193
9. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.finalGeometry_fields_rank_lt line 241
10. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.finalGeometry_code_rank_lt line 250
11. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.finalInclusions_rank_lt line 254
12. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.finalGeometry_below line 263
13. theorem OAI.PartitionPilot.Forcing.GroundMainFinalGeometry.exists_rowPositionSequences line 279
14. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.exists_finalRowPositionSequences line 316
15. theorem OAI.PartitionPilot.Forcing.GroundMainFinalGeometry.exists_smallRowTupleTerms line 343