OAI/SetTheory/PartitionPrinciple/Forcing/RenamedPairNameFamilies.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_uniformRename_between line 12
  2. def OAI.PartitionPilot.Forcing.Name.renameFamilyGraph line 106
  3. def OAI.PartitionPilot.Forcing.Name.renamedFamily line 111
  4. theorem OAI.PartitionPilot.Forcing.Name.mem_renameFamilyGraph line 115
  5. theorem OAI.PartitionPilot.Forcing.Name.pair_mem_renameFamilyGraph line 126
  6. theorem OAI.PartitionPilot.Forcing.Name.renameFamilyGraph_function line 139
  7. theorem OAI.PartitionPilot.Forcing.Name.mem_renamedFamily line 151
  8. def OAI.PartitionPilot.Forcing.SetFormula.renamedNameFamilyPairFormula line 166
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.renameFamilyGraph_mem line 183
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.renamedFamily_mem line 231
  11. def OAI.PartitionPilot.Forcing.SetFormula.termActionEntryFormula line 247
  12. def OAI.PartitionPilot.Forcing.SetFormula.termActionSetFormula line 251
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_termActionEntryFormula line 268
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_termActionSetFormula line 302
  15. theorem OAI.PartitionPilot.Forcing.PosetAction.support_of_term_graphs line 326
  16. theorem OAI.PartitionPilot.Forcing.PosetAction.positionSupport_of_term_graphs line 340
  17. theorem OAI.PartitionPilot.Forcing.Name.renamedFamily_valid line 362
  18. theorem OAI.PartitionPilot.Forcing.Name.presentationFamily_injection line 369
  19. theorem OAI.PartitionPilot.Forcing.Name.rename_familySet line 382
  20. theorem OAI.PartitionPilot.Forcing.Name.eval_renamedFamily line 398
  21. theorem OAI.PartitionPilot.Forcing.Name.renamedFamily_closed line 413
  22. theorem OAI.PartitionPilot.Forcing.Name.renamedFamily_hs line 424
  23. def OAI.PartitionPilot.Forcing.SetFormula.termActionFamilyEntryFormula line 440
  24. def OAI.PartitionPilot.Forcing.PosetAction.termActionFamily line 448
  25. theorem OAI.PartitionPilot.Forcing.PosetAction.pair_mem_termActionFamily line 452
  26. theorem OAI.PartitionPilot.Forcing.PosetAction.termActionFamily_function line 458
  27. theorem OAI.PartitionPilot.Forcing.TransitiveGround.termActionFamily_mem line 482
  28. theorem OAI.PartitionPilot.Forcing.Name.renamedFamily_orderedPairNameFamily line 545
  29. theorem OAI.PartitionPilot.Forcing.Name.renamedFamily_iteratedPairNameFamily line 573