OAI/SetTheory/PartitionPrinciple/Forcing/GroundExternalOldAction.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalCopyGraph_eq_graphline 26 - theorem
OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalCopy_idealline 42 - theorem
OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalIdentityCopy_idealline 64 - theorem
OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalIdentityCopy_equivariantline 97 - theorem
OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalIdentityCopy_agreementline 123 - theorem
OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalOriginal_agreementline 144