OAI/SetTheory/PartitionPrinciple/Geometry/GroundNormalizedRefinementOutputs.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PartitionPilot.Forcing.equivalenceClass_empty_of_not_memline 12 - structure
OAI.PartitionPilot.Forcing.RefinementObjectValuesline 21 - def
OAI.PartitionPilot.Forcing.TransitiveGround.refinementNameEnvline 51 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.refinementObjects_evalline 56 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.normalizedRefinementOutputsline 112