OAI/SetTheory/PartitionPrinciple/Transfinite/LimitProfilePersistence.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.lastCone line 14
2. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.union_bottom_same line 19
3. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.unionBottom line 31
4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.unionBottom_at line 35
5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.unionBottom_least line 39
6. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.limitHeight line 47
7. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.limit line 52
8. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.limitTransition line 67
9. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.limitCone line 76
10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.limit_strict_top line 83
11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.limit_point_cover line 87
12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.limit_actor_cover line 95
13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.limit_height_stage line 98
14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.FixedTop.preservesProfiles line 109
15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.union_preservesProfiles line 121
16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.limit_preservesProfiles line 133