OAI/SetTheory/PartitionPrinciple/Geometry/RequestedOwnerSlotLaws.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Request.vertexSlot line 16
2. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Request.vertexSlot_lt_three line 22
3. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Request.vertexSlot_injective line 31
4. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.VertexSlotSupports line 61
5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.vertexSlotSupports_bound line 65
6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.vertexSlotSupports_cover line 70
7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.vertexSlotSupports_lower line 75
8. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.leastVertexSlot line 82
9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.leastVertexSlot_support line 86
10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.leastVertexSlot_lt_three line 91
11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.leastVertexSlot_le line 95
12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.leastVertexSlot_eq_iff line 100
13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.leastVertexSlot_mono line 112
14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.leastSupport_meet_depth_lt line 128
15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.owner_meet_depth_lt line 141
16. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.SlotSupports line 153
17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.slotSupports_iff line 157
18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.slotSupports_placed_iff line 166
19. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.slotSupports_bound line 177
20. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.slotSupports_lower line 182
21. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.slotSupports_tile line 189
22. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.tile_slot_cover line 194
23. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.fresh_owner_slot_cover line 199
24. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.slotSupports_owner_cutoff line 206