OAI/SetTheory/PartitionPrinciple/Definability/ParentSupportCodes.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.BoundedFormula.orderedRightTripleFormula line 11
  2. def OAI.PartitionPilot.Forcing.BoundedFormula.rightTripleMembershipFormula line 15
  3. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_orderedRightTripleFormula line 18
  4. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_rightTripleMembershipFormula line 34
  5. def OAI.PartitionPilot.Forcing.BoundedFormula.relationToProductFormula line 46
  6. def OAI.PartitionPilot.Forcing.BoundedFormula.functionToProductFormula line 50
  7. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_relationToProductFormula line 58
  8. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_functionToProductFormula line 72
  9. structure OAI.PartitionPilot.Forcing.ChoiceFunctionCode line 108
  10. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_nonemptyFormula line 116
  11. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_choiceFunctionFormula line 121
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.choice_witness line 159
  13. def OAI.PartitionPilot.Forcing.relationFiber line 182
  14. theorem OAI.PartitionPilot.Forcing.mem_relationFiber line 185
  15. def OAI.PartitionPilot.Forcing.choiceUniformGraph line 188
  16. theorem OAI.PartitionPilot.Forcing.pair_mem_choiceUniformGraph line 192
  17. theorem OAI.PartitionPilot.Forcing.choiceUniformGraph_function line 203
  18. def OAI.PartitionPilot.Forcing.BoundedFormula.fiberFormula line 220
  19. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_fiberFormula line 225
  20. def OAI.PartitionPilot.Forcing.BoundedFormula.choiceUniformEntryFormula line 242
  21. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_choiceUniformEntryFormula line 248
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.relationFiber_mem line 269
  23. def OAI.PartitionPilot.Forcing.TransitiveGround.nonemptyGroundSubsets line 282
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_nonemptyGroundSubsets line 285
  25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.nonemptyGroundSubsets_mem line 290
  26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.choiceUniformGraph_mem line 303
  27. theorem OAI.PartitionPilot.Forcing.TransitiveGround.uniformize_relation line 321
  28. def OAI.PartitionPilot.Forcing.BoundedFormula.relationFiberFamilyEntryFormula line 352
  29. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_relationFiberFamilyEntryFormula line 356
  30. def OAI.PartitionPilot.Forcing.TransitiveGround.relationFiberFamily line 369
  31. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_relationFiberFamily line 373
  32. theorem OAI.PartitionPilot.Forcing.TransitiveGround.relationFiberFamily_mem line 390
  33. theorem OAI.PartitionPilot.Forcing.TransitiveGround.relationFiberFamily_function line 407
  34. theorem OAI.PartitionPilot.Forcing.TransitiveGround.relationFiberFamily_entries line 419
  35. def OAI.PartitionPilot.Forcing.ExternalCosetSupport line 436
  36. def OAI.PartitionPilot.Forcing.ExternalTileSupport line 440
  37. def OAI.PartitionPilot.Forcing.externalStarSupportGraph line 444
  38. theorem OAI.PartitionPilot.Forcing.pair_mem_externalStarSupportGraph line 449
  39. def OAI.PartitionPilot.Forcing.BoundedFormula.externalCosetSupportFormula line 463
  40. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalCosetSupportFormula line 469
  41. def OAI.PartitionPilot.Forcing.BoundedFormula.externalTileSupportFormula line 476
  42. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalTileSupportFormula line 482
  43. def OAI.PartitionPilot.Forcing.BoundedFormula.externalStarSupportEntryFormula line 489
  44. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalStarSupportEntryFormula line 496
  45. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalStarSupportGraph_mem line 512
  46. def OAI.PartitionPilot.Forcing.parentSupportGraph line 543
  47. def OAI.PartitionPilot.Forcing.freshSupportGraph line 547
  48. theorem OAI.PartitionPilot.Forcing.pair_mem_parentSupportGraph line 550
  49. theorem OAI.PartitionPilot.Forcing.pair_mem_parentSupportGraph_of_parent line 561
  50. theorem OAI.PartitionPilot.Forcing.pair_mem_freshSupportGraph line 574
  51. def OAI.PartitionPilot.Forcing.BoundedFormula.parentSupportEntryFormula line 580
  52. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_parentSupportEntryFormula line 586
  53. theorem OAI.PartitionPilot.Forcing.TransitiveGround.parentSupportGraph_mem line 607
  54. theorem OAI.PartitionPilot.Forcing.TransitiveGround.freshSupportGraph_mem line 622