OAI/SetTheory/PartitionPrinciple/Definability/GroundMainFinalGraphValueCandidateAvailability.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.TransitiveGround.graphValueCandidateCodes line 14
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_graphValueCandidateCodes line 18
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.graphValueCandidateCodes_hs line 26
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.translated_descendant_mem_graphValueCandidates line 35
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.graphValueCandidateCodes_mem line 42
6. def OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalSupportFulfillment.GraphValueCandidateDensity line 70
7. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalSupportFulfillment.graphValueCandidateDensity_of_compression line 79
8. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalSupportFulfillment.structural_graphValue_candidates_dense line 127
9. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalSupportFulfillment.structural_graphValue_candidate_availability line 256