OAI/SetTheory/PartitionPrinciple/Geometry/FinalProfilePersistence.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.FinalPoint line 13
2. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.FinalActor line 14
3. instance OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.finalGroup line 16
4. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.finalOrder line 19
5. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.finalAction line 21
6. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.finalHeight line 24
7. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.finalBottom line 27
8. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.finalBottom_least line 29
9. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.finalInclusion line 32
10. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.finalGroupInclusion line 35
11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.finalGroupInclusion_injective line 38
12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.final_points_coherent line 41
13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.final_actors_coherent line 45
14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.final_point_cover line 49
15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.final_actor_cover line 52
16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.final_height_stage line 55
17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.final_action_stage line 58
18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.final_agreement line 63
19. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.final_no_maximal line 71
20. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.final_no_greatest line 83
21. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transition.preservesProfiles_transport line 98
22. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.ordinalStep_preservesProfiles line 106
23. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.transition_preservesProfiles_at line 129
24. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.final_preservesProfiles line 147