OAI/SetTheory/PartitionPrinciple/Transfinite/RecursiveLiftAgreement.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.recursiveAttachmentIndices line 14
  2. theorem OAI.PartitionPilot.Forcing.recursiveAttachmentIndices_subset line 19
  3. theorem OAI.PartitionPilot.Forcing.pair_mem_recursiveAttachmentIndices line 23
  4. def OAI.PartitionPilot.Forcing.pairFieldGraph line 35
  5. theorem OAI.PartitionPilot.Forcing.pair_mem_pairFieldGraph line 40
  6. theorem OAI.PartitionPilot.Forcing.pairFieldGraph_entry_iff line 52
  7. theorem OAI.PartitionPilot.Forcing.pairFieldGraph_function line 64
  8. def OAI.PartitionPilot.Forcing.BoundedFormula.recursiveAttachmentIndexFormula line 88
  9. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_recursiveAttachmentIndexFormula line 94
  10. def OAI.PartitionPilot.Forcing.BoundedFormula.pairFieldEntryFormula line 104
  11. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_pairFieldEntryFormula line 110
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.recursiveAttachmentIndices_mem line 127
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pairFieldGraph_mem line 149
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pairFieldGraph_spec line 171
  15. def OAI.PartitionPilot.Forcing.pairSecondField line 198
  16. def OAI.PartitionPilot.Forcing.pairFirstField line 201
  17. def OAI.PartitionPilot.Forcing.recursiveSeparatorFamily line 204
  18. theorem OAI.PartitionPilot.Forcing.pairSecondField_entry_iff line 208
  19. theorem OAI.PartitionPilot.Forcing.pairFirstField_entry_iff line 216
  20. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.separator_function line 224
  21. theorem OAI.PartitionPilot.Forcing.recursiveSeparatorFamily_function line 233
  22. theorem OAI.PartitionPilot.Forcing.recursiveSeparatorFamily_entry_iff line 244
  23. theorem OAI.PartitionPilot.Forcing.recursiveAttachmentIndices_entry_iff line 258
  24. theorem OAI.PartitionPilot.Forcing.recursiveFresh_iff line 278
  25. theorem OAI.PartitionPilot.Forcing.recursiveFresh_shape line 294
  26. theorem OAI.PartitionPilot.Forcing.negativeRecursiveFresh_mem line 304
  27. theorem OAI.PartitionPilot.Forcing.TransitiveGround.recursiveSeparatorFamily_mem line 327
  28. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundRecursiveBatchInputs line 340
  29. structure OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs line 402
  30. def OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.source line 423
  31. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.source_entry line 427
  32. def OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.actor line 431
  33. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.actor_entry line 435
  34. def OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.previous line 438
  35. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.previous_entry line 443
  36. def OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.representative line 450
  37. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.representative_entry line 465
  38. def OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.toInputs line 477
  39. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.toInputs_source line 490
  40. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.toInputs_previous_entry line 492
  41. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.toInputs_representative_entry line 497
  42. abbrev OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextIndices line 517
  43. abbrev OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.NextInputs line 520
  44. def OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextIndex line 528
  45. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextIndex_injective line 534
  46. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextIndex_surjective line 543
  47. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.next_space line 556
  48. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.next_rel line 562
  49. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.next_meet line 568
  50. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.next_anchor line 574
  51. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.next_embed line 580
  52. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.next_filter line 587
  53. def OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextFresh line 594
  54. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextFresh_injective line 601
  55. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextFresh_surjective line 609
  56. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextFresh_inside_iff line 622
  57. abbrev OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.liftGraph line 655
  58. abbrev OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.liftSection line 659
  59. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.liftGraph_function line 662
  60. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.liftSection_function line 672
  61. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.liftGraph_old_iff line 676
  62. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.liftGraph_positive_iff line 686
  63. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.liftGraph_negative_iff line 709
  64. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.liftGraph_agrees_on_base line 734
  65. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.liftSection_agrees_on_base line 752