OAI/SetTheory/PartitionPrinciple/Models/GroundSuccessorInjections.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.setSuccessor_injective line 10
2. theorem OAI.PartitionPilot.Forcing.setSuccessor_ne_empty line 21
3. def OAI.PartitionPilot.Forcing.shiftedInjectionGraph line 25
4. theorem OAI.PartitionPilot.Forcing.mem_shiftedInjectionGraph line 29
5. theorem OAI.PartitionPilot.Forcing.pair_mem_shiftedInjectionGraph line 40
6. theorem OAI.PartitionPilot.Forcing.shiftedInjectionGraph_no_zero line 51
7. theorem OAI.PartitionPilot.Forcing.InjectionCode.shift line 59
8. def OAI.PartitionPilot.Forcing.adjoinInjectionGraph line 77
9. theorem OAI.PartitionPilot.Forcing.pair_mem_adjoinInjectionGraph line 80
10. theorem OAI.PartitionPilot.Forcing.InjectionCode.adjoin_fresh line 87
11. def OAI.PartitionPilot.Forcing.BoundedFormula.shiftedInjectionEntryFormula line 132
12. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_shiftedInjectionEntryFormula line 138
13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.insert_mem line 162
14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.shiftedInjectionGraph_mem line 174
15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.adjoinInjectionGraph_mem line 201
16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEmbeddable_insert line 212