OAI/SetTheory/PartitionPrinciple/Definability/ExternalGroupOperationGraphs.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.TransitiveGround.externalGroupPresentation line 21
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalGroupPresentation_carrier line 25
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalGroupPresentation_encode_evalWord line 31
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalGroupClassifier_eq_graph line 43
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalGroupPresentation_ground line 61
6. def OAI.PartitionPilot.Forcing.TransitiveGround.externalGroupCarrier line 81
7. def OAI.PartitionPilot.Forcing.TransitiveGround.externalGroupProjection line 85
8. def OAI.PartitionPilot.Forcing.TransitiveGround.externalGroupMultiplication line 89
9. def OAI.PartitionPilot.Forcing.TransitiveGround.externalGroupInverse line 94
10. def OAI.PartitionPilot.Forcing.TransitiveGround.externalGroupIdentity line 99
11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalGroupOperations_ground line 109
12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalGroupMultiplication_eq_graph line 132
13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalGroupInverse_eq_graph line 152
14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalGroupIdentity_eq_encode line 168