OAI/SetTheory/PartitionPrinciple/Definability/GroundSemanticStructuralFamilyEvaluation.lean
10 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralPrefixMembershipName_evalline 79 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralPrefixMembershipName_groundline 222 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralPrefixRefinementEnvironmentline 334 - def
OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralNameLiftline 443 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralNameLift_valline 447 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralNameLift_memline 453 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralNameLift_evalline 458 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralNameLiftGraph_eqline 463 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralNameLiftGraph_memline 478 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralPowerFamily_eval_prefixline 560