OAI/SetTheory/PartitionPrinciple/Definability/GroundPairCompositions.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.FunctionGraphOn.value line 13
  2. theorem OAI.PartitionPilot.Forcing.FunctionGraphOn.value_entry line 16
  3. theorem OAI.PartitionPilot.Forcing.FunctionGraphOn.value_eq_of_entry line 20
  4. theorem OAI.PartitionPilot.Forcing.FunctionGraphOn.value_mem_doubleUnion line 24
  5. theorem OAI.PartitionPilot.Forcing.FunctionGraphOn.value_mem line 28
  6. def OAI.PartitionPilot.Forcing.FunctionGraphOn.totalValue line 36
  7. theorem OAI.PartitionPilot.Forcing.FunctionGraphOn.totalValue_entry line 40
  8. theorem OAI.PartitionPilot.Forcing.FunctionGraphOn.totalValue_eq_of_entry line 45
  9. theorem OAI.PartitionPilot.Forcing.FunctionGraphOn.totalValue_outside line 49
  10. theorem OAI.PartitionPilot.Forcing.FunctionGraphOn.totalValue_ground line 52
  11. def OAI.PartitionPilot.Forcing.productFirst line 69
  12. def OAI.PartitionPilot.Forcing.productSecond line 72
  13. theorem OAI.PartitionPilot.Forcing.mem_productFirst line 75
  14. theorem OAI.PartitionPilot.Forcing.mem_productSecond line 87
  15. theorem OAI.PartitionPilot.Forcing.productFirst_function line 99
  16. theorem OAI.PartitionPilot.Forcing.productSecond_function line 102
  17. def OAI.PartitionPilot.Forcing.BoundedFormula.productFirstEntryFormula line 109
  18. def OAI.PartitionPilot.Forcing.BoundedFormula.productSecondEntryFormula line 112
  19. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_productFirstEntryFormula line 115
  20. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_productSecondEntryFormula line 120
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.productFirst_mem line 132
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.productSecond_mem line 149
  23. theorem OAI.PartitionPilot.Forcing.relationCompose_domain_eq line 176
  24. def OAI.PartitionPilot.Forcing.pairCompositionFamily line 188
  25. theorem OAI.PartitionPilot.Forcing.pair_mem_pairCompositionFamily line 194
  26. theorem OAI.PartitionPilot.Forcing.pairCompositionFamily_entry_iff line 210
  27. theorem OAI.PartitionPilot.Forcing.pairCompositionFamily_function line 224
  28. def OAI.PartitionPilot.Forcing.BoundedFormula.compositionGraphFormula line 244
  29. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_compositionGraphFormula line 250
  30. def OAI.PartitionPilot.Forcing.BoundedFormula.pairCompositionEntryFormula line 270
  31. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_pairCompositionEntryFormula line 279
  32. def OAI.PartitionPilot.Forcing.literalTaskCode line 300
  33. def OAI.PartitionPilot.Forcing.literalTaskBound line 303
  34. theorem OAI.PartitionPilot.Forcing.literalTaskCode_inj line 306
  35. theorem OAI.PartitionPilot.Forcing.literalTaskCode_mem_bound line 311
  36. theorem OAI.PartitionPilot.Forcing.mem_literalTaskBound line 316
  37. def OAI.PartitionPilot.Forcing.literalTaskField line 332
  38. theorem OAI.PartitionPilot.Forcing.literalTaskField_map line 335
  39. def OAI.PartitionPilot.Forcing.literalTaskFieldBound line 342
  40. theorem OAI.PartitionPilot.Forcing.literalTaskField_mem line 345
  41. def OAI.PartitionPilot.Forcing.literalTaskFieldGraph line 352
  42. theorem OAI.PartitionPilot.Forcing.mem_literalTaskFieldGraph line 359
  43. theorem OAI.PartitionPilot.Forcing.pair_mem_literalTaskFieldGraph line 371
  44. theorem OAI.PartitionPilot.Forcing.literalTaskFieldGraph_entry_iff line 385
  45. theorem OAI.PartitionPilot.Forcing.literalTaskFieldGraph_function line 400
  46. abbrev OAI.PartitionPilot.Forcing.literalTaskSourceGraph line 413
  47. abbrev OAI.PartitionPilot.Forcing.literalTaskTargetGraph line 415
  48. abbrev OAI.PartitionPilot.Forcing.literalTaskBaseGraph line 417
  49. abbrev OAI.PartitionPilot.Forcing.literalTaskSeparatorGraph line 419
  50. abbrev OAI.PartitionPilot.Forcing.literalTaskFilterGraph line 421
  51. abbrev OAI.PartitionPilot.Forcing.literalTaskLabelGraph line 423
  52. def OAI.PartitionPilot.Forcing.constantFamilyGraph line 426
  53. theorem OAI.PartitionPilot.Forcing.pair_mem_constantFamilyGraph line 428
  54. theorem OAI.PartitionPilot.Forcing.constantFamilyGraph_function line 432
  55. def OAI.PartitionPilot.Forcing.BoundedFormula.literalTaskFormula line 443
  56. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_literalTaskFormula line 454
  57. def OAI.PartitionPilot.Forcing.BoundedFormula.literalTaskFieldEntryFormula line 481
  58. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_literalTaskFieldEntryFormula line 489
  59. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pairCompositionFamily_mem line 513
  60. def OAI.PartitionPilot.Forcing.TransitiveGround.groundPairCompositions line 539
  61. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundPairCompositions_spec line 542