OAI/SetTheory/PartitionPrinciple/Geometry/GroundOrdinarySubmodelReflection.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryExtension line 15
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_ordinaryExtension line 18
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ground_subset_ordinaryExtension line 23
4. def OAI.PartitionPilot.Forcing.GroundSequenceReflection line 42
5. theorem OAI.PartitionPilot.Forcing.GroundSequenceReflection.enumeration line 50
6. theorem OAI.PartitionPilot.Forcing.GroundSequenceReflection.countable_subset line 77
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinary_ZF_of_conditionMaps line 128
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinary_collection_of_conditionMaps line 146
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryExtension_ZF line 166
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryExtension_collection line 175
11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.visibleSupportProfile_mem_ordinary line 202
12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_forced_visibleSupportProfile line 258
13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryExtension_sequenceReflection line 293
14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryExtension_submodel_sequenceReflection line 310