OAI/SetTheory/PartitionPrinciple/Forcing/GroundRowGenerics.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.BoundedFormula.coordinateAssignedFormula line 12
2. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_coordinateAssignedFormula line 15
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.coordinateAssigned_code_mem line 29
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.generic_meets_coordinate line 62
5. def OAI.PartitionPilot.Forcing.TransitiveGround.countableGenericGraph line 89
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_countableGenericGraph line 95
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.countableGenericGraph_extends line 107
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.countableGenericGraph_partial line 115
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.countableGenericGraph_isFunc line 131
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_total_countableFunction_generic line 151
11. def OAI.PartitionPilot.Forcing.BoundedFormula.rowDistinguishingFormula line 180
12. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_rowDistinguishingFormula line 186
13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rowDistinguishing_code_mem line 203
14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.generic_meets_rowDistinguishing line 237
15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.countableGenericGraph_rows_separated line 259