OAI/SetTheory/PartitionPrinciple/Definability/ExternalTileSlotSupportRealization.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalTileSlotPointsline 12 - theorem
OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalTileSlotPoints_entryline 48 - theorem
OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalTileSlotPoints_groundline 88 - theorem
OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalTileSlotPoints_decodeline 96 - theorem
OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalTileSlotPoints_owner_coverline 126 - theorem
OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalTileSlotPoints_lowerline 137