OAI/SetTheory/PartitionPrinciple/Definability/GroundSemanticStructuralDataSupport.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralCurrent_witness line 41
  2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralCurrent_stage line 57
  3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_semanticStructuralFinalHistory line 84
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralAction_code line 165
  5. def OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralAction line 173
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralAction_graph line 183
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralAction_coordinates line 190
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralAction_sourceCondition line 272
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralCurrent_assignment_fixed_of_dataBound line 340
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralAssignment_relationLaws line 496
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralAssignmentImage_eq_of_fixed line 505
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralAction_fixed_iff line 525
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralAssignment_fixed_of_dataBound line 581
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralAssignmentImage_eq_of_dataBound line 686
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralCondition_fixed_of_dataBound line 697