OAI/SetTheory/PartitionPrinciple/Definability/GroundRegularFormulas.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.SetFormula.cumulativeHierarchyFormula line 14
2. def OAI.PartitionPilot.Forcing.SetFormula.cumulativeLevelFormula line 17
3. def OAI.PartitionPilot.Forcing.SetFormula.cumulativeRankLtFormula line 23
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_cumulativeHierarchyFormula line 30
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_cumulativeLevelFormula_iff_graph line 44
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_cumulativeLevelFormula line 76
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_cumulativeRankLtFormula line 95
8. def OAI.PartitionPilot.Forcing.GroundRegular line 119
9. theorem OAI.PartitionPilot.Forcing.GroundRegular.bound_small_domain line 130
10. theorem OAI.PartitionPilot.Forcing.GroundRegular.bound_paired line 151
11. def OAI.PartitionPilot.Forcing.SetFormula.cumulativeRankValueFormula line 176
12. def OAI.PartitionPilot.Forcing.SetFormula.cumulativeRankEntryFormula line 182
13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_cumulativeRankValueFormula line 196
14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_cumulativeRankEntryFormula line 240
15. def OAI.PartitionPilot.Forcing.SetFormula.groundRegularFormula line 273
16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_groundRegularFormula line 283
17. def OAI.PartitionPilot.Forcing.cumulativeRankGraph line 318
18. theorem OAI.PartitionPilot.Forcing.pair_mem_cumulativeRankGraph line 322
19. theorem OAI.PartitionPilot.Forcing.cumulativeRankGraph_function line 333
20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.cumulativeRankGraph_mem line 348
21. theorem OAI.PartitionPilot.Forcing.GroundRegular.bound_rank_family line 383
22. theorem OAI.PartitionPilot.Forcing.GroundRegular.rank_lt_of_small line 398