OAI/SetTheory/PartitionPrinciple/Geometry/DirectSystem.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem line 11
2. def OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.Label line 22
3. def OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.Related line 23
4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.related_refl line 26
5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.related_symm line 27
6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.related_trans line 31
7. def OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.setoid line 44
8. def OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.Union line 45
9. def OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.point line 46
10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.point_map line 48
11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.point_injective line 53
12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.cover line 58
13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.pair_cover line 62
14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.triple_cover line 69
15. def OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.descend line 76
16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.descend_point line 83
17. def OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.binaryLabel line 92
18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.binaryLabel_at line 98
19. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.binaryLabel_respects line 104
20. def OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.binary line 116
21. theorem OAI.PartitionPilot.Compression.RecursiveMaps.DirectSystem.binary_point line 120