OAI/SetTheory/PartitionPrinciple/Definability/PrincipalTileRealization.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.CodedPrincipalTile.decode line 15
2. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.encode_decode line 18
3. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.decode_encode line 21
4. def OAI.PartitionPilot.Forcing.CodedPrincipalTile.encodingIso line 24
5. def OAI.PartitionPilot.Forcing.CodedPrincipalTile.decodingIso line 28
6. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.encodingIso_value line 31
7. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.decodingIso_encode line 34
8. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.vertex_cover line 37
9. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.cross_meet_entry line 45
10. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.old_graph_ideal line 53
11. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.template_graph_ideal line 60