OAI/SetTheory/PartitionPrinciple/Definability/TileStarIncidenceRealization.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.tileStar_source_entry line 23
2. theorem OAI.PartitionPilot.Forcing.tileStar_source_entry_iff line 42
3. theorem OAI.PartitionPilot.Forcing.tileStar_source_iff line 84
4. theorem OAI.PartitionPilot.Forcing.tileStar_reverse_iff line 93
5. theorem OAI.PartitionPilot.Forcing.tileStar_target_iff line 115
6. theorem OAI.PartitionPilot.Forcing.presentedGraph_eq line 133
7. theorem OAI.PartitionPilot.Forcing.tileStar_endpoint_graphs line 150
8. theorem OAI.PartitionPilot.Forcing.tileStar_endpoint_functions line 167
9. theorem OAI.PartitionPilot.Forcing.tileStar_incidence_iff line 179
10. theorem OAI.PartitionPilot.Forcing.tileStar_adjacency_iff line 188