OAI/Computability/WitnessedChoice/FormTransfer.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.WitnessedSeparation.Forms.Domain line 22
  2. def OAI.WitnessedSeparation.Forms.Cell line 25
  3. def OAI.WitnessedSeparation.Forms.cellEquiv line 42
  4. theorem OAI.WitnessedSeparation.Forms.cell_finite line 52
  5. theorem OAI.WitnessedSeparation.Forms.supported_domain_bijection line 62
  6. inductive OAI.WitnessedSeparation.Forms.HFRelation line 167
  7. def OAI.WitnessedSeparation.Forms.hfStructure line 170
  8. def OAI.WitnessedSeparation.Forms.Represented line 176
  9. def OAI.WitnessedSeparation.Forms.twoBlocks line 185
  10. theorem OAI.WitnessedSeparation.Forms.comp_twoBlocks line 196
  11. def OAI.WitnessedSeparation.Forms.splitBlock line 200
  12. theorem OAI.WitnessedSeparation.Forms.represented_equal line 221
  13. theorem OAI.WitnessedSeparation.Forms.represented_mem line 232
  14. theorem OAI.WitnessedSeparation.Forms.represented_atom line 245
  15. theorem OAI.WitnessedSeparation.Forms.base_value line 252
  16. theorem OAI.WitnessedSeparation.Forms.represented_base line 267
  17. theorem OAI.WitnessedSeparation.Forms.splitBlock_symm_new line 288
  18. theorem OAI.WitnessedSeparation.Forms.splitBlock_symm_old line 292
  19. theorem OAI.WitnessedSeparation.Forms.homogeneity_reindex line 296
  20. theorem OAI.WitnessedSeparation.Forms.represented_extension line 315
  21. theorem OAI.WitnessedSeparation.Forms.supported_eval_transfer line 365
  22. theorem OAI.WitnessedSeparation.Forms.supported_sentences_transfer line 392
  23. def OAI.WitnessedSeparation.Forms.namesOfCard line 429
  24. def OAI.WitnessedSeparation.Forms.HomogeneousThrough line 432
  25. theorem OAI.WitnessedSeparation.Forms.homogeneous_tuple line 438
  26. theorem OAI.WitnessedSeparation.Forms.hf_transfer line 446
  27. theorem OAI.WitnessedSeparation.Hereditary.supports_pad line 486
  28. theorem OAI.WitnessedSeparation.Grid.central_smul_HF line 511
  29. theorem OAI.WitnessedSeparation.Grid.small_orbit_supported line 514
  30. theorem OAI.WitnessedSeparation.Grid.orbit_card_le_invariant_family line 529
  31. theorem OAI.WitnessedSeparation.Grid.invariant_family_hereditarily_supported line 541
  32. theorem OAI.WitnessedSeparation.Grid.atom_nonempty line 571
  33. instance OAI.WitnessedSeparation.Grid.atom_nonempty_succ line 574
  34. theorem OAI.WitnessedSeparation.Grid.central_analysis_isomorphism line 576
  35. theorem OAI.WitnessedSeparation.Grid.homogeneous_through_numeric line 580
  36. theorem OAI.WitnessedSeparation.Grid.base_empty_type line 592
  37. theorem OAI.WitnessedSeparation.Grid.grid_hf_transfer line 605
  38. structure OAI.WitnessedSeparation.Interpretations.Structure line 632
  39. inductive OAI.WitnessedSeparation.Interpretations.Formula line 639
  40. def OAI.WitnessedSeparation.Interpretations.Formula.eval line 648
  41. def OAI.WitnessedSeparation.Interpretations.Formula.holds line 660
  42. structure OAI.WitnessedSeparation.Interpretations.Interpretation line 663
  43. abbrev OAI.WitnessedSeparation.Interpretations.Interpretation.Domain line 672
  44. def OAI.WitnessedSeparation.Interpretations.Interpretation.link line 674
  45. def OAI.WitnessedSeparation.Interpretations.Interpretation.classSetoid line 677
  46. abbrev OAI.WitnessedSeparation.Interpretations.Interpretation.Vertex line 680
  47. def OAI.WitnessedSeparation.Interpretations.Interpretation.apply line 682
  48. structure OAI.WitnessedSeparation.Interpretations.Program line 696
  49. def OAI.WitnessedSeparation.Interpretations.Program.state line 708
  50. def OAI.WitnessedSeparation.Interpretations.Program.haltsAt line 712
  51. def OAI.WitnessedSeparation.Interpretations.Program.cost line 715
  52. def OAI.WitnessedSeparation.Interpretations.Program.accepts line 718
  53. def OAI.WitnessedSeparation.Interpretations.Program.polynomiallyBounded line 721
  54. def OAI.WitnessedSeparation.Interpretations.Program.decides line 725
  55. def OAI.WitnessedSeparation.Interpretations.NondefinableByInterpretations line 730
  56. def OAI.WitnessedSeparation.Interpretations.payload line 745
  57. theorem OAI.WitnessedSeparation.Interpretations.mem_payload line 749
  58. theorem OAI.WitnessedSeparation.Interpretations.payload_injective line 755
  59. def OAI.WitnessedSeparation.Interpretations.vertexCode line 768
  60. theorem OAI.WitnessedSeparation.Interpretations.vertexCode_injective line 771
  61. def OAI.WitnessedSeparation.Interpretations.pairFamily line 776
  62. def OAI.WitnessedSeparation.Interpretations.classFamily line 779
  63. theorem OAI.WitnessedSeparation.Interpretations.pairFamily_card_le line 783
  64. theorem OAI.WitnessedSeparation.Interpretations.classFamily_card_le line 795
  65. theorem OAI.WitnessedSeparation.Interpretations.stage_family_transitive line 806
  66. def OAI.WitnessedSeparation.Counting.Definable line 851
  67. theorem OAI.WitnessedSeparation.Counting.Definable.congr line 859
  68. theorem OAI.WitnessedSeparation.Counting.Definable.reindex line 864
  69. theorem OAI.WitnessedSeparation.Counting.Definable.falsum line 873
  70. theorem OAI.WitnessedSeparation.Counting.Definable.neg line 877
  71. theorem OAI.WitnessedSeparation.Counting.Definable.and line 882
  72. theorem OAI.WitnessedSeparation.Counting.Definable.or line 889
  73. theorem OAI.WitnessedSeparation.Counting.Definable.imp line 893
  74. theorem OAI.WitnessedSeparation.Counting.Definable.iff line 897
  75. theorem OAI.WitnessedSeparation.Counting.Definable.equal line 901
  76. theorem OAI.WitnessedSeparation.Counting.Definable.relation line 907
  77. theorem OAI.WitnessedSeparation.Counting.Definable.fresh line 913
  78. theorem OAI.WitnessedSeparation.Counting.Definable.updated_args line 923
  79. theorem OAI.WitnessedSeparation.Counting.Definable.free_binder line 931
  80. theorem OAI.WitnessedSeparation.Counting.Definable.ex line 941
  81. theorem OAI.WitnessedSeparation.Counting.Definable.all line 952
  82. theorem OAI.WitnessedSeparation.Counting.Definable.exact line 956
  83. theorem OAI.WitnessedSeparation.Counting.Definable.exists_finset line 967
  84. theorem OAI.WitnessedSeparation.Counting.Definable.bounded_hartig line 975