OAI/SetTheory/PartitionPrinciple/Transfinite/RecursiveNextMapInputs.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundRecursiveAttachment line 14
2. abbrev OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.groundLiftFamily line 81
3. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.groundLiftFamily_spec line 85
4. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.exists_groundLiftGraphs line 110
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEligibleRecursiveAttachment line 147
6. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.exists_groundLiftEmbeddings line 231
7. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.sources_on_current line 274
8. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextMapInputs_of_family line 280
9. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.ground_nextMapInputs line 296