OAI/SetTheory/PartitionPrinciple/Geometry/GroundRowDistinguishing.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.rowCoordinateDomain line 12
2. def OAI.PartitionPilot.Forcing.rowUsedColumns line 15
3. theorem OAI.PartitionPilot.Forcing.mem_rowCoordinateDomain line 18
4. theorem OAI.PartitionPilot.Forcing.rowCoordinateDomain_subset line 33
5. theorem OAI.PartitionPilot.Forcing.mem_rowUsedColumns line 37
6. theorem OAI.PartitionPilot.Forcing.rowUsedColumns_subset line 53
7. theorem OAI.PartitionPilot.Forcing.not_mem_rowUsedColumns_iff line 56
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rowCoordinateDomain_mem line 74
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rowUsedColumns_mem line 84
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rowCoordinateDomain_groundEmbeddable line 94
11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rowUsedColumns_groundEmbeddable line 107
12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_fresh_rowColumn line 120
13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.countablePartialFunctions_fresh_column line 139
14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.countablePartialFunctions_insert_two_rows line 166
15. def OAI.PartitionPilot.Forcing.TransitiveGround.rowDistinguishing line 189
16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rowDistinguishing_dense line 195
17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rowDistinguishing_downward line 231