OAI/SetTheory/PartitionPrinciple/Geometry/PartialBatchStep.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.Present line 12
2. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.present_down line 16
3. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.Cutoff line 30
4. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.cutoffOrder line 32
5. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.cutoffEmbedding line 43
6. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.cutoffOld line 49
7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.present_tile line 57
8. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.cutoffTile line 64
9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.present_mono line 73
10. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.cutoffInclusion line 79
11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.cutoffInclusion_coherent line 86
12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.cutoff_no_new_below line 91
13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.cutoff_cover line 95
14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.outside_greatest_part line 116
15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.outside_meet line 133
16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.present_unselected_tile line 148
17. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.addComponent line 158
18. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.stepInput line 160
19. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.stepMap line 167
20. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.stepMap_le line 171
21. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.stepMap_surjective line 185
22. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.stepEmbedding line 196
23. def OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.stepIso line 201
24. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.stepIso_old line 209
25. theorem OAI.PartitionPilot.Compression.RecursiveMaps.PrincipalBatch.Family.stepIso_tile line 213