OAI/SetTheory/PartitionPrinciple/Forcing/GroundCompleteProjectionGenericity.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.TransitiveGround.codedFamily line 16
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.codedFamily_countable line 18
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.codedFamily_of_code line 21
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_ground_generic line 27
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.generic_meets_coded_dense line 31
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.symmetric_names_countable line 36
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_joint_generic line 41
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_joint_projection_generic line 69
9. theorem OAI.PartitionPilot.Forcing.SetFormula.forces_iff_all_generics line 119
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryForces_iff_all_generics line 141
11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_coded_ordinary_generic line 161
12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryForces_iff_all_joint_generics line 173
13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryForces_congr_equalities line 200
14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryForces_replace_first line 222
15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinary_generic_meets_coded_dense line 244
16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinary_generic_meets_ground_dense line 283
17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.completeProjection_codedGeneric line 310