OAI/SetTheory/PartitionPrinciple/Definability/GroundLiftedCompressionFormulas.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.SetFormula.sectionFamilyEntryFormula line 11
2. def OAI.PartitionPilot.Forcing.SetFormula.sectionFamilyFormula line 16
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_sectionFamilyEntryFormula line 26
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_sectionFamilyFormula line 59
5. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_liftedCompressionEntryFormula_mem line 78
6. def OAI.PartitionPilot.Forcing.SetFormula.liftedCompressionGraphFormula line 97
7. def OAI.PartitionPilot.Forcing.SetFormula.liftedCompressionFamilyFormula line 103
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_liftedCompressionGraphFormula line 116
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_liftedCompressionFamilyFormula line 138