OAI/SetTheory/PartitionPrinciple/Forcing/GroundDefinableRefinementNameGraphs.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.Name.refinementOutput line 12
2. def OAI.PartitionPilot.Forcing.SetFormula.refinementOutputCodeFormula line 20
3. def OAI.PartitionPilot.Forcing.TransitiveGround.refinementNameBound line 29
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementNameBound_mem line 33
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementOutput_mem_bound line 51
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_refinementOutputCodeFormula line 77
7. def OAI.PartitionPilot.Forcing.SetFormula.refinementIndexNameGraphFormula line 114
8. def OAI.PartitionPilot.Forcing.TransitiveGround.refinementIndexNameGraph line 129
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementIndexNameGraph_mem line 135
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_refinementIndexNameGraphFormula line 150
11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementIndexNameGraph_entry line 182
12. def OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementNameGraph line 251
13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndex_field_entry line 263
14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementNameGraph_mem line 289
15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementNameGraph_entry line 296
16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementNameGraph_function line 311
17. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_refinementNameBound line 341
18. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_refinementIndexNameGraph line 350