OAI/SetTheory/PartitionPrinciple/Definability/GroundBelowFunctionGraphs.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.functionCode_partial line 10
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEmbeddable_function_image line 22
3. theorem OAI.PartitionPilot.Forcing.GroundBelow.of_witness line 63
4. theorem OAI.PartitionPilot.Forcing.GroundBelow.bound_mono line 66
5. theorem OAI.PartitionPilot.Forcing.GroundBelow.of_inclusion line 70
6. theorem OAI.PartitionPilot.Forcing.GroundBelow.empty_iff line 75
7. theorem OAI.PartitionPilot.Forcing.GroundBelow.restrict line 82
8. theorem OAI.PartitionPilot.Forcing.GroundBelow.of_embeddable line 87
9. theorem OAI.PartitionPilot.Forcing.GroundBelow.function_image line 99
10. def OAI.PartitionPilot.Forcing.SetFormula.groundBelowFormula line 115
11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_groundBelowFormula line 123
12. def OAI.PartitionPilot.Forcing.functionSourceProjection line 148
13. theorem OAI.PartitionPilot.Forcing.pair_mem_functionSourceProjection line 151
14. theorem OAI.PartitionPilot.Forcing.functionSourceProjection_injection line 162
15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.functionSourceProjection_mem line 187
16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.functionGraph_embeds_source line 192
17. theorem OAI.PartitionPilot.Forcing.GroundBelow.functionGraphOn line 203
18. theorem OAI.PartitionPilot.Forcing.GroundBelow.functionGraph line 212