OAI/ModelTheory/Choiceless/Interpretations.lean

GitHub source file

112 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CPTSeparation.Interpretations.Structure line 9
  2. inductive OAI.CPTSeparation.Interpretations.Formula line 16
  3. def OAI.CPTSeparation.Interpretations.Formula.eval line 25
  4. def OAI.CPTSeparation.Interpretations.Formula.holds line 37
  5. structure OAI.CPTSeparation.Interpretations.Interpretation line 40
  6. abbrev OAI.CPTSeparation.Interpretations.Interpretation.Domain line 49
  7. def OAI.CPTSeparation.Interpretations.Interpretation.link line 51
  8. def OAI.CPTSeparation.Interpretations.Interpretation.classSetoid line 54
  9. abbrev OAI.CPTSeparation.Interpretations.Interpretation.Vertex line 57
  10. def OAI.CPTSeparation.Interpretations.Interpretation.apply line 59
  11. structure OAI.CPTSeparation.Interpretations.Program line 73
  12. def OAI.CPTSeparation.Interpretations.Program.state line 85
  13. def OAI.CPTSeparation.Interpretations.Program.haltsAt line 89
  14. def OAI.CPTSeparation.Interpretations.Program.cost line 92
  15. def OAI.CPTSeparation.Interpretations.Program.accepts line 95
  16. def OAI.CPTSeparation.Interpretations.Program.polynomiallyBounded line 98
  17. def OAI.CPTSeparation.Interpretations.Program.decides line 102
  18. def OAI.CPTSeparation.Interpretations.NondefinableByInterpretations line 107
  19. theorem OAI.CPTSeparation.Hereditary.ofFinset_inj line 118
  20. def OAI.CPTSeparation.Hereditary.singleton line 121
  21. def OAI.CPTSeparation.Hereditary.pair line 123
  22. theorem OAI.CPTSeparation.Hereditary.mem_singleton line 125
  23. theorem OAI.CPTSeparation.Hereditary.mem_double line 127
  24. theorem OAI.CPTSeparation.Hereditary.singleton_inj line 129
  25. theorem OAI.CPTSeparation.Hereditary.map_singleton line 131
  26. theorem OAI.CPTSeparation.Hereditary.map_double line 133
  27. theorem OAI.CPTSeparation.Hereditary.map_pair line 139
  28. theorem OAI.CPTSeparation.Hereditary.pair_injective line 141
  29. theorem OAI.CPTSeparation.Hereditary.pair_eq_pair line 162
  30. theorem OAI.CPTSeparation.Hereditary.ordinal_isSet line 165
  31. theorem OAI.CPTSeparation.Hereditary.mem_ordinal line 167
  32. theorem OAI.CPTSeparation.Hereditary.ordinal_injective line 184
  33. theorem OAI.CPTSeparation.Hereditary.map_ordinal line 195
  34. def OAI.CPTSeparation.Hereditary.wrappers line 205
  35. theorem OAI.CPTSeparation.Hereditary.wrappers_card_le line 207
  36. theorem OAI.CPTSeparation.Hereditary.wrappers_trans line 210
  37. def OAI.CPTSeparation.Interpretations.payload line 228
  38. theorem OAI.CPTSeparation.Interpretations.mem_payload line 232
  39. theorem OAI.CPTSeparation.Interpretations.payload_injective line 238
  40. def OAI.CPTSeparation.Interpretations.vertexCode line 251
  41. theorem OAI.CPTSeparation.Interpretations.vertexCode_injective line 254
  42. def OAI.CPTSeparation.Interpretations.pairFamily line 259
  43. def OAI.CPTSeparation.Interpretations.classFamily line 262
  44. theorem OAI.CPTSeparation.Interpretations.pairFamily_card_le line 266
  45. theorem OAI.CPTSeparation.Interpretations.classFamily_card_le line 278
  46. theorem OAI.CPTSeparation.Interpretations.stage_family_transitive line 289
  47. def OAI.CPTSeparation.Counting.Definable line 328
  48. theorem OAI.CPTSeparation.Counting.Definable.congr line 336
  49. theorem OAI.CPTSeparation.Counting.Definable.reindex line 341
  50. theorem OAI.CPTSeparation.Counting.Definable.falsum line 350
  51. theorem OAI.CPTSeparation.Counting.Definable.neg line 354
  52. theorem OAI.CPTSeparation.Counting.Definable.and line 359
  53. theorem OAI.CPTSeparation.Counting.Definable.or line 366
  54. theorem OAI.CPTSeparation.Counting.Definable.imp line 370
  55. theorem OAI.CPTSeparation.Counting.Definable.iff line 374
  56. theorem OAI.CPTSeparation.Counting.Definable.equal line 378
  57. theorem OAI.CPTSeparation.Counting.Definable.relation line 384
  58. theorem OAI.CPTSeparation.Counting.Definable.fresh line 390
  59. theorem OAI.CPTSeparation.Counting.Definable.updated_args line 400
  60. theorem OAI.CPTSeparation.Counting.Definable.free_binder line 408
  61. theorem OAI.CPTSeparation.Counting.Definable.ex line 418
  62. theorem OAI.CPTSeparation.Counting.Definable.all line 429
  63. theorem OAI.CPTSeparation.Counting.Definable.exact line 433
  64. theorem OAI.CPTSeparation.Counting.Definable.exists_finset line 444
  65. theorem OAI.CPTSeparation.Counting.Definable.bounded_hartig line 452
  66. abbrev OAI.CPTSeparation.HFCoding.Domain line 471
  67. def OAI.CPTSeparation.HFCoding.SingletonTest line 477
  68. def OAI.CPTSeparation.HFCoding.DoubleTest line 480
  69. theorem OAI.CPTSeparation.HFCoding.singletonTest_iff line 485
  70. theorem OAI.CPTSeparation.HFCoding.doubleTest_iff line 504
  71. def OAI.CPTSeparation.HFCoding.PairTest line 526
  72. theorem OAI.CPTSeparation.HFCoding.pairTest_iff line 529
  73. theorem OAI.CPTSeparation.HFCoding.singleton_value_definable line 551
  74. theorem OAI.CPTSeparation.HFCoding.singleton_definable line 563
  75. theorem OAI.CPTSeparation.HFCoding.double_value_definable line 568
  76. theorem OAI.CPTSeparation.HFCoding.double_definable line 580
  77. theorem OAI.CPTSeparation.HFCoding.pair_definable line 585
  78. theorem OAI.CPTSeparation.HFCoding.ordinal_definable line 597
  79. def OAI.CPTSeparation.Counting.UniformDefinable line 635
  80. theorem OAI.CPTSeparation.Counting.UniformDefinable.congr line 643
  81. theorem OAI.CPTSeparation.Counting.UniformDefinable.reindex line 649
  82. theorem OAI.CPTSeparation.Counting.UniformDefinable.falsum line 658
  83. theorem OAI.CPTSeparation.Counting.UniformDefinable.neg line 661
  84. theorem OAI.CPTSeparation.Counting.UniformDefinable.and line 666
  85. theorem OAI.CPTSeparation.Counting.UniformDefinable.or line 673
  86. theorem OAI.CPTSeparation.Counting.UniformDefinable.imp line 677
  87. theorem OAI.CPTSeparation.Counting.UniformDefinable.iff line 681
  88. theorem OAI.CPTSeparation.Counting.UniformDefinable.equal line 685
  89. theorem OAI.CPTSeparation.Counting.UniformDefinable.relation line 691
  90. theorem OAI.CPTSeparation.Counting.UniformDefinable.fresh line 698
  91. theorem OAI.CPTSeparation.Counting.UniformDefinable.updated_args line 708
  92. theorem OAI.CPTSeparation.Counting.UniformDefinable.free_binder line 716
  93. theorem OAI.CPTSeparation.Counting.UniformDefinable.ex line 726
  94. theorem OAI.CPTSeparation.Counting.UniformDefinable.all line 737
  95. theorem OAI.CPTSeparation.Counting.UniformDefinable.exact line 741
  96. theorem OAI.CPTSeparation.Counting.UniformDefinable.exists_finset line 752
  97. theorem OAI.CPTSeparation.Counting.UniformDefinable.bounded_hartig line 760
  98. theorem OAI.CPTSeparation.HFCoding.uniform_singleton line 789
  99. theorem OAI.CPTSeparation.HFCoding.uniform_double line 798
  100. theorem OAI.CPTSeparation.HFCoding.uniform_pair line 811
  101. theorem OAI.CPTSeparation.HFCoding.uniform_ordinal line 823
  102. structure OAI.CPTSeparation.Interpretations.Structure.Iso line 861
  103. def OAI.CPTSeparation.Interpretations.Structure.Iso.symm line 869
  104. theorem OAI.CPTSeparation.Interpretations.Structure.Iso.eval line 873
  105. def OAI.CPTSeparation.Interpretations.Interpretation.domainEquiv line 903
  106. theorem OAI.CPTSeparation.Interpretations.Interpretation.domainEquiv_val line 910
  107. theorem OAI.CPTSeparation.Interpretations.Interpretation.link_equiv line 913
  108. theorem OAI.CPTSeparation.Interpretations.Interpretation.eqvGen_map line 920
  109. theorem OAI.CPTSeparation.Interpretations.Interpretation.class_equiv line 930
  110. def OAI.CPTSeparation.Interpretations.Interpretation.vertexEquiv line 941
  111. theorem OAI.CPTSeparation.Interpretations.Interpretation.vertexEquiv_mk line 943
  112. def OAI.CPTSeparation.Interpretations.Interpretation.applyIso line 946