OAI/Computability/DirectedFeedback/Games/MatrixChartDegreeNeighbors.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Inverse.MatrixChart.HyperplanesBelow line 12
  2. abbrev OAI.DFVSGames.Inverse.MatrixChart.GrassmannNeighbors line 15
  3. def OAI.DFVSGames.Inverse.MatrixChart.hyperplanesBelowEquiv line 19
  4. theorem OAI.DFVSGames.Inverse.MatrixChart.inf_eq_base_of_distinct_extensions line 34
  5. abbrev OAI.DFVSGames.Inverse.MatrixChart.NeighborExtensionData line 51
  6. def OAI.DFVSGames.Inverse.MatrixChart.neighborsEquivExtensionData line 54
  7. theorem OAI.DFVSGames.Inverse.MatrixChart.card_other_extensions_binary line 76
  8. theorem OAI.DFVSGames.Inverse.MatrixChart.card_grassmann_neighbors_binary line 102
  9. def OAI.DFVSGames.Inverse.KMSBasisComparison.rankOneUpdate line 134
  10. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.rankOneUpdate_apply line 137
  11. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.rankOneUpdate_mem_range_iff line 140
  12. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.injective_rankOneUpdate line 154
  13. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.range_inf_rankOneUpdate line 165
  14. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.comap_range_inf_rankOneUpdate line 181
  15. def OAI.DFVSGames.Inverse.KMSBasisComparison.rankOneUpdateNeighbor line 189
  16. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.rankOneUpdateNeighbor_val line 203
  17. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.exists_functional_ker_eq line 219
  18. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.exists_rankOneUpdate_range_eq line 231
  19. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.rankOneUpdateNeighbor_surjective line 280
  20. def OAI.DFVSGames.Inverse.MatrixChart.graphEquiv line 296
  21. theorem OAI.DFVSGames.Inverse.MatrixChart.graph_injective line 310
  22. theorem OAI.DFVSGames.Inverse.MatrixChart.exists_unique_graph_iff line 317
  23. def OAI.DFVSGames.Inverse.MatrixChart.intersectionEquiv line 329
  24. theorem OAI.DFVSGames.Inverse.MatrixChart.finrank_graph line 349
  25. theorem OAI.DFVSGames.Inverse.MatrixChart.finrank_intersection_add_rank line 353
  26. theorem OAI.DFVSGames.Inverse.MatrixChart.adjacent_iff_rank_one line 359
  27. theorem OAI.DFVSGames.Inverse.MatrixChart.adjacent_rank_one_step line 366
  28. def OAI.DFVSGames.Inverse.MatrixChart.lowerRows line 378
  29. theorem OAI.DFVSGames.Inverse.MatrixChart.lowerRows_le_graph_iff line 381
  30. def OAI.DFVSGames.Inverse.MatrixChart.upperColumns line 391
  31. theorem OAI.DFVSGames.Inverse.MatrixChart.graph_le_upperColumns_iff line 396
  32. theorem OAI.DFVSGames.Inverse.MatrixChart.interval_iff_slice line 413
  33. theorem OAI.DFVSGames.Inverse.MatrixChart.exists_smulRight_of_rank_one line 428
  34. theorem OAI.DFVSGames.Inverse.MatrixChart.rank_one_iff_exists_smulRight line 452
  35. theorem OAI.DFVSGames.Inverse.MatrixChart.binary_smulRight_unique line 467
  36. abbrev OAI.DFVSGames.Inverse.MatrixChart.BinaryRankOneFactors line 487
  37. abbrev OAI.DFVSGames.Inverse.MatrixChart.BinaryRankOneMaps line 492
  38. def OAI.DFVSGames.Inverse.MatrixChart.binaryRankOneMap line 497
  39. theorem OAI.DFVSGames.Inverse.MatrixChart.binary_smulRight_injective line 502
  40. theorem OAI.DFVSGames.Inverse.MatrixChart.binary_smulRight_surjective line 509
  41. def OAI.DFVSGames.Inverse.MatrixChart.binaryRankOneEquiv line 515
  42. theorem OAI.DFVSGames.Inverse.MatrixChart.binaryRankOneEquiv_apply line 520
  43. theorem OAI.DFVSGames.Inverse.MatrixChart.card_binaryRankOneMaps line 523
  44. theorem OAI.DFVSGames.Inverse.MatrixChart.card_binaryRankOneMaps_pow line 534
  45. theorem OAI.DFVSGames.Inverse.MatrixChart.card_binaryRankOneMaps_coordinates line 546
  46. abbrev OAI.DFVSGames.Inverse.KMSBasisComparison.FixedFunctionalNeighborFiber line 565
  47. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.add_image_not_mem_range line 570
  48. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.range_update_add_kernel line 575
  49. def OAI.DFVSGames.Inverse.KMSBasisComparison.fixedFunctionalFiberMap line 593
  50. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.fixedFunctionalFiberMap_injective line 599
  51. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.fixedFunctionalFiberMap_surjective line 608
  52. def OAI.DFVSGames.Inverse.KMSBasisComparison.fixedFunctionalNeighborFiberEquiv line 637
  53. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.card_fixedFunctionalNeighborFiber line 645
  54. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.card_fixedFunctionalNeighborFiber_pow line 651
  55. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.binary_functional_eq_of_ker_eq line 673
  56. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.binary_functional_eq_of_map_ker_eq line 687
  57. abbrev OAI.DFVSGames.Inverse.KMSBasisComparison.OutsideNeighborFactors line 702
  58. abbrev OAI.DFVSGames.Inverse.KMSBasisComparison.OutsideNeighborPairFiber line 705
  59. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.functional_eq_of_update_range_eq line 710
  60. def OAI.DFVSGames.Inverse.KMSBasisComparison.fixedToPairFiber line 718
  61. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.fixedToPairFiber_injective line 723
  62. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.fixedToPairFiber_surjective line 730
  63. def OAI.DFVSGames.Inverse.KMSBasisComparison.fixedFunctionalEquivPairFiber line 746
  64. def OAI.DFVSGames.Inverse.KMSBasisComparison.outsideNeighborPairFiberEquiv line 754
  65. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.card_outsideNeighborPairFiber line 761