OAI/SetTheory/PartitionPrinciple/Forcing/GroundProductActions.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.SetFormula.renameStateFormula line 12
  2. def OAI.PartitionPilot.Forcing.SetFormula.renameCertificateFormula line 15
  3. def OAI.PartitionPilot.Forcing.TransitiveGround.renameParameters line 25
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_renameState line 28
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rawRenameStep_names line 50
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_renameState_names line 79
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.renameCertificate_sound line 99
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_renameState_fixedPoint line 123
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundRename_certificate line 145
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rename_eq_iff_exists_certificate line 174
  11. def OAI.PartitionPilot.Forcing.SetFormula.binaryApplication line 199
  12. theorem OAI.PartitionPilot.Forcing.SetFormula.realize_binaryApplication line 202
  13. def OAI.PartitionPilot.Forcing.SetFormula.uniformRenameFormula line 208
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_uniformRenameFormula line 220
  15. def OAI.PartitionPilot.Forcing.PosetAction.conditionMapFamily line 252
  16. theorem OAI.PartitionPilot.Forcing.PosetAction.pair_mem_conditionMapFamily line 255
  17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.conditionMap_graph_mem line 275
  18. def OAI.PartitionPilot.Forcing.PosetAction.actionGraph line 289
  19. theorem OAI.PartitionPilot.Forcing.PosetAction.triple_mem_actionGraph line 292
  20. def OAI.PartitionPilot.Forcing.PosetActionCode.act line 305
  21. theorem OAI.PartitionPilot.Forcing.PosetActionCode.act_mem line 309
  22. theorem OAI.PartitionPilot.Forcing.PosetActionCode.act_eq_iff line 314
  23. theorem OAI.PartitionPilot.Forcing.PosetActionCode.act_one line 319
  24. theorem OAI.PartitionPilot.Forcing.PosetActionCode.act_mul line 328
  25. theorem OAI.PartitionPilot.Forcing.PosetActionCode.act_inv_left line 337
  26. theorem OAI.PartitionPilot.Forcing.PosetActionCode.act_inv_right line 343
  27. theorem OAI.PartitionPilot.Forcing.PosetActionCode.act_monotone line 349
  28. theorem OAI.PartitionPilot.Forcing.PosetActionCode.act_le_iff line 358
  29. def OAI.PartitionPilot.Forcing.PosetActionCode.toPosetAction line 371
  30. theorem OAI.PartitionPilot.Forcing.PosetActionCode.actionGraph_eq line 387
  31. def OAI.PartitionPilot.Forcing.identityPosetAction line 405
  32. def OAI.PartitionPilot.Forcing.trivialGroupPresentation line 410
  33. theorem OAI.PartitionPilot.Forcing.identityPosetAction_graph_eq line 418
  34. theorem OAI.PartitionPilot.Forcing.identityPosetAction_conditionMapFamily line 431
  35. theorem OAI.PartitionPilot.Forcing.TransitiveGround.trivialGroupPresentation_mem line 452
  36. theorem OAI.PartitionPilot.Forcing.TransitiveGround.identityPosetAction_conditionMapFamily_mem line 459
  37. def OAI.PartitionPilot.Forcing.SetFormula.nameActionFormula line 481
  38. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_nameActionFormula line 494
  39. def OAI.PartitionPilot.SetRealization.Presentation.nonbottom line 536
  40. theorem OAI.PartitionPilot.SetRealization.Presentation.nonbottom_encode line 549
  41. theorem OAI.PartitionPilot.SetRealization.Presentation.mem_nonbottom_carrier line 552
  42. def OAI.PartitionPilot.Forcing.PosetAction.nonbottomIso line 564
  43. def OAI.PartitionPilot.Forcing.PosetAction.nonbottom line 574
  44. theorem OAI.PartitionPilot.Forcing.PosetAction.nonbottom_iso_val line 579
  45. def OAI.PartitionPilot.Forcing.BoundedFormula.actionRestrictionEntryFormula line 589
  46. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_actionRestrictionEntryFormula line 593
  47. theorem OAI.PartitionPilot.Forcing.PosetAction.nonbottom_actionGraph_eq_sep line 608
  48. theorem OAI.PartitionPilot.Forcing.TransitiveGround.nonbottom_carrier_mem line 647
  49. theorem OAI.PartitionPilot.Forcing.TransitiveGround.nonbottom_actionGraph_mem line 654
  50. def OAI.PartitionPilot.Forcing.PosetAction.productColumns line 676
  51. theorem OAI.PartitionPilot.Forcing.PosetAction.productColumns_apply line 689
  52. theorem OAI.PartitionPilot.Forcing.PosetAction.mem_productColumns_actionGraph line 692
  53. def OAI.PartitionPilot.Forcing.BoundedFormula.productColumnsEntryFormula line 712
  54. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_productColumnsEntryFormula line 720
  55. theorem OAI.PartitionPilot.Forcing.BoundedFormula.productColumnsEntry_correct line 732
  56. theorem OAI.PartitionPilot.Forcing.TransitiveGround.productColumns_actionGraph_mem line 769