OAI/SetTheory/PartitionPrinciple/Geometry/GroundMainTransitionValidity.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PartitionPilot.Forcing.GroundMainTransition.lawsline 14 - def
OAI.PartitionPilot.Forcing.GroundMainTransition.ofLawsline 22 - theorem
OAI.PartitionPilot.Forcing.GroundMainTransition.ofLaws_codeline 40 - theorem
OAI.PartitionPilot.Forcing.GroundMainTransition.ofLaws_selfline 48 - theorem
OAI.PartitionPilot.Forcing.GroundMainTransition.exists_code_iffline 52 - def
OAI.PartitionPilot.Forcing.BoundedFormula.validMainTransitionCodeFormulaline 70 - theorem
OAI.PartitionPilot.Forcing.BoundedFormula.truth_validMainTransitionCodeFormulaline 77 - theorem
OAI.PartitionPilot.Forcing.BoundedFormula.realize_validMainTransitionCodeFormulaline 89