OAI/SetTheory/PartitionPrinciple/Definability/BoundedChronologyCodes.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.BoundedFormula.oldMeetFormula line 11
2. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_oldMeetFormula line 23
3. def OAI.PartitionPilot.Forcing.BoundedFormula.birthBoundFormula line 39
4. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_birthBoundFormula line 43
5. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_oldMeetFormula line 52
6. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_birthBoundFormula line 59