OAI/SetTheory/PartitionPrinciple/Models/RootedGluingQuotient.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.Label line 12
2. inductive OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.Related line 14
3. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.labelSetoid line 22
4. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.Generated line 23
5. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.labelClass line 24
6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.label_parent line 26
7. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.stageClass line 31
8. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.stageClass_old line 36
9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.stageClass_vertex line 39
10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.stageClass_up line 68
11. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.toGenerated line 76
12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.toGenerated_vertex line 82
13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.related_sound line 86
14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.exact_identifications line 94
15. def OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.fromGenerated line 103
16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.from_to line 106
17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.to_from line 111