OAI/SetTheory/PartitionPrinciple/Forcing/GroundFlatSuccessorFullActionGraph.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_actionSectionEntry line 14
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_actionSection line 24
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.actionGraph_section_mem line 34
4. def OAI.PartitionPilot.Forcing.TransitiveGround.smallFunctionAction line 74
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.raw_smallFunctionAction line 107
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.smallFunctionAction_entry line 112
7. def OAI.PartitionPilot.Forcing.SetFormula.actionMapPairFormula line 129
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_actionMapPairFormula line 142
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.conditionMapFamily_mem_of_actionGraph line 176
10. structure OAI.PartitionPilot.Forcing.StageOneActionParameters line 215
11. def OAI.PartitionPilot.Forcing.rowPositionSequenceAction line 231
12. theorem OAI.PartitionPilot.Forcing.pair_mem_rowPositionSequenceAction line 236
13. theorem OAI.PartitionPilot.Forcing.rowPositionSequenceAction_function line 253
14. theorem OAI.PartitionPilot.Forcing.rowPositionSequenceAction_code line 278
15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rowPositionSequenceAction_mem line 302
16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.decoded_conditionMapFamily_mem line 331
17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_ZF_interpretation_from_actionGraph line 353
18. def OAI.PartitionPilot.Forcing.TransitiveGround.flatSuccessorFullActionGraph line 388
19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.flatSuccessorFullActionGraph_entry line 392
20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.flatSuccessorFullActionGraph_mem line 414