OAI/SetTheory/PartitionPrinciple/Definability/GroundAssignmentClassGraphs.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.SetFormula.refinementClassCodeFormula line 10
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_refinementClassCodeFormula line 17
3. def OAI.PartitionPilot.Forcing.assignmentClassGraphFormula line 39
4. def OAI.PartitionPilot.Forcing.TransitiveGround.assignmentClassGraph line 53
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.assignmentClassGraph_mem line 58
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_assignmentClassGraphFormula line 72
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.assignmentClassGraph_entry line 103
8. def OAI.PartitionPilot.Forcing.SetFormula.refinementMapEntryFormula line 165
9. def OAI.PartitionPilot.Forcing.SetFormula.refinementMapCodeFormula line 174
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_refinementMapEntryFormula line 187
11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_refinementMapCodeFormula line 281
12. def OAI.PartitionPilot.Forcing.SetFormula.refinementQuotientEntryFormula line 301
13. def OAI.PartitionPilot.Forcing.SetFormula.refinementQuotientCodeFormula line 308
14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_refinementQuotientEntryFormula line 321
15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_refinementQuotientCodeFormula line 378