OAI/SetTheory/PartitionPrinciple/Definability/GroundCompositionFamilyFormulas.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PartitionPilot.Forcing.SetFormula.compositionFamilyEntryFormulaline 12 - def
OAI.PartitionPilot.Forcing.SetFormula.compositionFamilyFormulaline 22 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.realize_compositionFamilyEntryFormulaline 32 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.realize_compositionFamilyFormulaline 68