OAI/SetTheory/PartitionPrinciple/Geometry/GroundProjectedRowUniqueFibers.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PartitionPilot.Forcing.TransitiveGround.completeProjection_codedGeneric_of_ordinaryline 12 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.completeProjection_binaryRowValues_neline 33 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.projectedBinaryRows_uniqueFiber_incompatibleline 87