OAI/Computability/DirectedFeedback/Games/ChildLifts.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Gadget.tupleEmbed line 17
  2. theorem OAI.DFVSGames.Gadget.tupleEmbed_single line 23
  3. theorem OAI.DFVSGames.Gadget.shiftAggregate_single line 30
  4. theorem OAI.DFVSGames.Gadget.parent_lift_common_child line 36
  5. theorem OAI.DFVSGames.Gadget.parent_lift_child_kernel line 63
  6. structure OAI.DFVSGames.Gadget.Lift line 83
  7. def OAI.DFVSGames.Gadget.Lift.restrict line 87
  8. def OAI.DFVSGames.Gadget.singleInput line 95
  9. def OAI.DFVSGames.Gadget.childCharacter line 101
  10. theorem OAI.DFVSGames.Gadget.exists_common_child_character line 110
  11. def OAI.DFVSGames.Gadget.descendantFamily line 126
  12. theorem OAI.DFVSGames.Gadget.exists_descendant_lift line 137
  13. theorem OAI.DFVSGames.Gadget.descendant_detection_implies_parent line 166
  14. theorem OAI.DFVSGames.Gadget.Orientation.sum_action_eq line 194
  15. theorem OAI.DFVSGames.Gadget.Orientation.card_mul_sum_action line 200
  16. theorem OAI.DFVSGames.Gadget.Orientation.mean_action line 218
  17. theorem OAI.DFVSGames.Gadget.Orientation.exists_map_eq_of_finrank_eq line 233
  18. theorem OAI.DFVSGames.Gadget.Orientation.rank_map line 250
  19. def OAI.DFVSGames.Gadget.Orientation.RankSpace line 254
  20. instance OAI.DFVSGames.Gadget.Orientation.rankSpaceAction line 257
  21. theorem OAI.DFVSGames.Gadget.Orientation.rankSpace_transitive line 266
  22. theorem OAI.DFVSGames.Gadget.Orientation.mean_oriented_subspace line 272
  23. theorem OAI.DFVSGames.Gadget.Orientation.rank_dual_pullback line 281
  24. def OAI.DFVSGames.Gadget.Orientation.orientationEquiv line 285
  25. theorem OAI.DFVSGames.Gadget.Orientation.mean_map_equiv line 291
  26. def OAI.DFVSGames.Gadget.Orientation.dualOrientationEquiv line 316
  27. theorem OAI.DFVSGames.Gadget.Orientation.mean_dual_pullback line 329
  28. theorem OAI.DFVSGames.Gadget.OrientationVectors.exists_equiv_map_nonzero line 359
  29. theorem OAI.DFVSGames.Gadget.OrientationVectors.equiv_apply_ne_zero line 369
  30. instance OAI.DFVSGames.Gadget.OrientationVectors.nonzeroAction line 376
  31. theorem OAI.DFVSGames.Gadget.OrientationVectors.nonzero_transitive line 381
  32. theorem OAI.DFVSGames.Gadget.OrientationVectors.mean_oriented_nonzero line 386
  33. theorem OAI.DFVSGames.Gadget.OrientationVectors.mean_iso_nonzero line 393
  34. abbrev OAI.DFVSGames.Quadratic.Vec line 418
  35. def OAI.DFVSGames.Quadratic.Q line 422
  36. def OAI.DFVSGames.Quadratic.D line 424
  37. def OAI.DFVSGames.Quadratic.dot line 428
  38. theorem OAI.DFVSGames.Quadratic.Q_zero line 430
  39. theorem OAI.DFVSGames.Quadratic.Q_add line 434
  40. theorem OAI.DFVSGames.Quadratic.D_zero_left line 438
  41. theorem OAI.DFVSGames.Quadratic.D_zero_right line 442
  42. theorem OAI.DFVSGames.Quadratic.D_comm line 446
  43. theorem OAI.DFVSGames.Quadratic.D_add_left line 450
  44. theorem OAI.DFVSGames.Quadratic.D_add_right line 454
  45. theorem OAI.DFVSGames.Quadratic.D_smul_left line 457
  46. theorem OAI.DFVSGames.Quadratic.D_smul_right line 461
  47. theorem OAI.DFVSGames.Quadratic.dot_zero_right line 464
  48. theorem OAI.DFVSGames.Quadratic.dot_zero_left line 465
  49. theorem OAI.DFVSGames.Quadratic.dot_add_right line 467
  50. theorem OAI.DFVSGames.Quadratic.dot_smul_right line 471
  51. theorem OAI.DFVSGames.Quadratic.dot_smul_left line 475
  52. def OAI.DFVSGames.Quadratic.line line 479
  53. def OAI.DFVSGames.Quadratic.hyperplane line 481
  54. theorem OAI.DFVSGames.Quadratic.mem_hyperplane line 491
  55. theorem OAI.DFVSGames.Quadratic.mem_line_iff line 493
  56. theorem OAI.DFVSGames.Quadratic.vec_add_self line 498
  57. theorem OAI.DFVSGames.Quadratic.D_eq_polar line 502
  58. theorem OAI.DFVSGames.Quadratic.cross_self_zero_inline_Block line 508
  59. theorem OAI.DFVSGames.Quadratic.D_smul_smul_zero line 514
  60. theorem OAI.DFVSGames.Quadratic.dot_D_smul line 518
  61. theorem OAI.DFVSGames.Quadratic.D_mem_hyperplane line 527
  62. theorem OAI.DFVSGames.Quadratic.D_eq_zero_of_mem_line line 532
  63. theorem OAI.DFVSGames.Quadratic.Q_add_of_mem_line line 538
  64. def OAI.DFVSGames.Quadratic.U line 544
  65. theorem OAI.DFVSGames.Quadratic.mem_U line 565
  66. theorem OAI.DFVSGames.Quadratic.pair_mem_U line 568
  67. theorem OAI.DFVSGames.Quadratic.mem_U_iff_exists line 575
  68. abbrev OAI.DFVSGames.Quadratic.FieldLine line 592
  69. def OAI.DFVSGames.Quadratic.lineGenerator line 596
  70. theorem OAI.DFVSGames.Quadratic.lineGenerator_ne_zero line 598
  71. theorem OAI.DFVSGames.Quadratic.line_lineGenerator line 601
  72. theorem OAI.DFVSGames.Quadratic.fieldLine_finrank line 604
  73. theorem OAI.DFVSGames.Quadratic.card_FieldLine line 609
  74. theorem OAI.DFVSGames.Quadratic.card_fieldLine_submodules line 615
  75. theorem OAI.DFVSGames.Quadratic.card_FieldLine_pos line 621
  76. theorem OAI.DFVSGames.Quadratic.reciprocal_card_FieldLine line 625
  77. abbrev OAI.DFVSGames.Quadratic.lineBinary line 637
  78. abbrev OAI.DFVSGames.Quadratic.hyperplaneBinary line 640
  79. theorem OAI.DFVSGames.Quadratic.Q_cancel_inline_BlockDimension line 644
  80. def OAI.DFVSGames.Quadratic.blockParametrization line 649
  81. def OAI.DFVSGames.Quadratic.dotLinear line 690
  82. theorem OAI.DFVSGames.Quadratic.dotLinear_apply line 696
  83. theorem OAI.DFVSGames.Quadratic.dotLinear_ker line 699
  84. theorem OAI.DFVSGames.Quadratic.dotLinear_surjective line 702
  85. theorem OAI.DFVSGames.Quadratic.finrank_hyperplane line 721
  86. theorem OAI.DFVSGames.Quadratic.finrank_line line 730
  87. theorem OAI.DFVSGames.Quadratic.finrank_lineBinary line 737
  88. theorem OAI.DFVSGames.Quadratic.finrank_hyperplaneBinary line 743
  89. theorem OAI.DFVSGames.Quadratic.finrank_U line 749
  90. theorem OAI.DFVSGames.Quadratic.finrank_U_eq_finrank_vec line 755