OAI/SetTheory/PartitionPrinciple/Models/GroundChoiceEnumerationSteps.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.enumerationRemainder line 11
2. theorem OAI.PartitionPilot.Forcing.mem_enumerationRemainder line 14
3. def OAI.PartitionPilot.Forcing.ChoiceEnumerationStep line 18
4. def OAI.PartitionPilot.Forcing.BoundedFormula.enumerationRemainderFormula line 24
5. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_enumerationRemainderFormula line 31
6. def OAI.PartitionPilot.Forcing.BoundedFormula.choiceEnumerationStepFormula line 51
7. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_choiceEnumerationStepFormula line 57
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.enumerationRemainder_mem line 77
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.choiceEnumerationStep_exists_unique line 94