OAI/SetTheory/PartitionPrinciple/Definability/GroundPowerImageGraphs.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.InjectionCode.relationImage_inj line 12
2. def OAI.PartitionPilot.Forcing.BoundedFormula.imageSetFormula line 35
3. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_imageSetFormula line 39
4. def OAI.PartitionPilot.Forcing.BoundedFormula.powerImageEntryFormula line 55
5. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_powerImageEntryFormula line 59
6. def OAI.PartitionPilot.Forcing.TransitiveGround.groundPowerImageGraph line 72
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_groundPowerImageGraph line 77
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_groundPowerImageGraph line 87
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundPowerImageGraph_mem line 98
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundPowerImageGraph_entry_iff line 119
11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundPowerImageGraph_function line 131
12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundPowerImageGraph_injection line 140