OAI/SetTheory/PartitionPrinciple/Definability/FlatLimitConditionFormulas.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.BoundedFormula.assignmentCutFormula line 12
2. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_assignmentCutFormula line 19
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_assignmentCutFormula line 45
4. def OAI.PartitionPilot.Forcing.SetFormula.historyCutEntryBody line 61
5. def OAI.PartitionPilot.Forcing.SetFormula.historyCutEntryFormula line 68
6. def OAI.PartitionPilot.Forcing.SetFormula.flatHistoryCutsFormula line 71
7. def OAI.PartitionPilot.Forcing.SetFormula.flatLimitConditionFormula line 75
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_historyCutEntryFormula line 86
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_flatHistoryCutsFormula line 118
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_flatLimitConditionFormula line 138