OAI/SetTheory/PartitionPrinciple/Definability/CompressionRequestRealization.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.generator_root_of_tile line 12
2. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.generator_root_meet_of_tile line 19
3. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.generator_children_meet_of_tile line 28
4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.generator_fixes_ideal_of_tile line 38
5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.identityCopy_preservesProfiles line 45
6. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.external_separation_fixes line 68
7. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.external_separation_meet line 78
8. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.external_compression_restriction line 93
9. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.external_compression_top line 102
10. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.external_rectangle_roots line 111
11. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.external_rectangle_children line 128
12. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.external_rectangle_root_meets line 149
13. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.external_rectangle_children_meet line 168