OAI/SetTheory/PartitionPrinciple/Geometry/MainInsertion.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.compressionActor line 13
2. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.compressionCap line 16
3. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.compression_internal line 19
4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.compression_below_cap line 35
5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.compression_agrees_ideal line 46
6. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.insertionDatum line 71
7. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.insertionTask line 80
8. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.insertionTask_injective line 87
9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.insertion_representative_fixes line 94
10. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transition.Inserts line 112
11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transition.inserts_transport line 123
12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.next_inserts line 133