OAI/SetTheory/PartitionPrinciple/Definability/GroundSemanticAssignmentLabelCanonicalSuccessors.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralPrefix_assignment_tests line 78
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralAssignmentLabel_subset_quotients line 206
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralAssignmentLabel_eval_successor_lift line 362
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.assignmentLabel_raw_congr line 464
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.decoded_order_heq line 503
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralAssignmentLabel_canonical_successor_name line 620