OAI/SetTheory/PartitionPrinciple/Forcing/RequestedSupportOwners.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.leastSupport_root_copy_iffline 15 - theorem
OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.leastSupport_coset_iffline 25 - theorem
OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.tile_depth_ne_zeroline 41 - theorem
OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.leastSupport_tile_iffline 46 - theorem
OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.leastSupport_casesline 53 - theorem
OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.new_point_has_fresh_tileline 68