OAI/SetTheory/PartitionPrinciple/Models/GroundOrdinalPartitionInjectionAssembly.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.SetFormula.definableRelationEntryFormula line 13
2. def OAI.PartitionPilot.Forcing.TransitiveGround.definableRelation line 22
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_definableRelation line 27
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_definableRelationEntryFormula line 39
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.definableRelation_mem line 62
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.choose_definable_relation line 82
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundNameSupportChoice line 115
8. def OAI.PartitionPilot.Forcing.BoundedFormula.coveringPositionFormula line 165
9. theorem OAI.PartitionPilot.Forcing.BoundedFormula.coveringPosition_meaning line 173
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundCoveringRowPositions line 195
11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.indexedInjectionCandidates line 288
12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinalPartition_injection_assembly line 378