OAI/SetTheory/PartitionPrinciple/Forcing/RefinementAssignmentLabelNames.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.Name.refinementClass line 13
  2. theorem OAI.PartitionPilot.Forcing.Name.entry_refinementClass line 17
  3. theorem OAI.PartitionPilot.Forcing.Name.refinementClass_subset line 28
  4. theorem OAI.PartitionPilot.Forcing.Name.eval_refinementClass line 35
  5. theorem OAI.PartitionPilot.Forcing.Name.act_refinementClass line 62
  6. theorem OAI.PartitionPilot.Forcing.Name.refinementClass_support line 79
  7. theorem OAI.PartitionPilot.Forcing.Name.refinementClass_hs line 88
  8. def OAI.PartitionPilot.Forcing.SetFormula.refinementClassEntryFormula line 108
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_refinementClassEntryFormula line 127
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementClass_eq_selection line 190
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementClass_mem line 211
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.eval_refinementClass line 222
  13. def OAI.PartitionPilot.Forcing.Name.refinementAssignmentLabel line 247
  14. theorem OAI.PartitionPilot.Forcing.Name.entry_refinementAssignmentLabel line 260
  15. theorem OAI.PartitionPilot.Forcing.Name.mem_eval_refinementAssignmentLabel line 278