OAI/SetTheory/PartitionPrinciple/Geometry/GroundExternalCompressionFieldRecognition.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PartitionPilot.Forcing.mem_externalCompressionFieldline 11 - def
OAI.PartitionPilot.Forcing.BoundedFormula.externalCompressionFieldEntryFormulaline 29 - theorem
OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalCompressionFieldEntryFormulaline 33 - def
OAI.PartitionPilot.Forcing.SetFormula.externalCompressionFieldFormulaline 47 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.realize_externalCompressionFieldFormulaline 61 - def
OAI.PartitionPilot.Forcing.TransitiveGround.definable_externalCompressionFieldline 85