OAI/SetTheory/PartitionPrinciple/Forcing/GroundMainFinalRowSupport.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalSupportFulfillment.ordinary_ZF_insertion_of_choice line 22
2. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalSupportFulfillment.ordinary_ZF_countable_localization line 52
3. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalSupportFulfillment.ordinary_insertion line 89
4. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalSupportFulfillment.ordinary_submodel_insertion line 133
5. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalSupportFulfillment.ordinary_submodel_countable_localization line 164
6. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalSupportFulfillment.symmetric_insertion line 201
7. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalSupportFulfillment.symmetric_countable_localization line 230
8. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalSupportFulfillment.row_symmetric_insertion line 262
9. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalSupportFulfillment.row_symmetric_countable_localization line 328