OAI/SetTheory/PartitionPrinciple/Geometry/MainDiagramGluing.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transition.transport line 13
2. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transition.transport_twice line 19
3. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transition.transport_comp line 24
4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transition.transport_injective line 29
5. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.restrictLE line 38
6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.restrictLE_self line 41
7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.restrictLE_comp line 43
8. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.transition_of_eq line 46
9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.ext_of_transport line 50
10. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.Compatible line 65
11. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.Compatible.stage line 70
12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.Compatible.stage_at line 73
13. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.Compatible.transition line 77
14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.Compatible.transition_at line 81
15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.Compatible.transition_self line 90
16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.Compatible.transition_comp line 95
17. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.Compatible.glue line 107
18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.Compatible.glue_restrict line 113