OAI/SetTheory/PartitionPrinciple/Geometry/GroundMainFinalRowOrdinaryZF.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.GroundMainFinalGeometry.decoded_directed line 17
2. theorem OAI.PartitionPilot.Forcing.GroundMainFinalGeometry.decoded_separating line 32
3. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalFulfillment.internalRow_bounds_with line 81
4. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalFulfillment.exists_rowModel line 135
5. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalFulfillment.exists_rowTermSystem line 189
6. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalFulfillment.decoded_strict_growth line 288
7. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalFulfillment.exists_commonPrincipalSupport_strict_extension line 305
8. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalFulfillment.exists_rowModel_sequenceReflection line 343
9. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalFulfillment.exists_rowModel_ordinaryZF line 394