OAI/SetTheory/PartitionPrinciple/Forcing/GroundSharedConditionalNames.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.SetFormula.sharedConditionFormula line 14
  2. theorem OAI.PartitionPilot.Forcing.SetFormula.realize_sharedConditionFormula line 18
  3. def OAI.PartitionPilot.Forcing.Name.sharedConditionName line 31
  4. theorem OAI.PartitionPilot.Forcing.Name.entry_sharedConditionName line 36
  5. theorem OAI.PartitionPilot.Forcing.Name.sharedConditionName_subset line 49
  6. theorem OAI.PartitionPilot.Forcing.Name.eval_sharedConditionName line 66
  7. theorem OAI.PartitionPilot.Forcing.Name.eval_sharedConditionName_of_true line 82
  8. theorem OAI.PartitionPilot.Forcing.Name.eval_sharedConditionName_of_subset line 97
  9. theorem OAI.PartitionPilot.Forcing.Name.eval_sharedConditionName_of_false line 114
  10. theorem OAI.PartitionPilot.Forcing.Name.sharedConditionName_act line 141
  11. theorem OAI.PartitionPilot.Forcing.Name.sharedConditionName_nice line 147
  12. theorem OAI.PartitionPilot.Forcing.Name.sharedConditionName_hs line 161
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.sharedConditionName_mem line 183
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.sharedConditionName_spec line 192
  15. def OAI.PartitionPilot.Forcing.Name.refinementConditionNames line 218
  16. theorem OAI.PartitionPilot.Forcing.Name.eval_refinementConditionNames_coherent line 224
  17. theorem OAI.PartitionPilot.Forcing.Name.eval_refinementConditionNames_valid line 250
  18. theorem OAI.PartitionPilot.Forcing.Name.eval_refinementConditionNames_of_valid line 270