OAI/SetTheory/PartitionPrinciple/Definability/GreedyAntichainStepFormulas.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.BoundedFormula.antichainBlockedFormula line 12
2. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_antichainBlockedFormula line 17
3. def OAI.PartitionPilot.Forcing.BoundedFormula.antichainEligibleFormula line 25
4. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_antichainEligibleFormula line 32
5. def OAI.PartitionPilot.Forcing.BoundedFormula.greedyAntichainStepFormula line 53
6. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_greedyAntichainStepFormula line 59