OAI/LinearAlgebra/RankMatching/Basic.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HahnWilson.RankMatching.Triangular line 16
  2. def OAI.HahnWilson.RankMatching.block line 18
  3. def OAI.HahnWilson.RankMatching.blockRank line 21
  4. def OAI.HahnWilson.RankMatching.weight line 23
  5. def OAI.HahnWilson.RankMatching.Matched line 27
  6. def OAI.HahnWilson.RankMatching.OldUnmatched line 29
  7. def OAI.HahnWilson.RankMatching.PriorAgreement line 33
  8. def OAI.HahnWilson.RankMatching.matchingCount line 36
  9. def OAI.HahnWilson.RankMatching.column line 41
  10. def OAI.HahnWilson.RankMatching.columnSpace line 44
  11. lemma OAI.HahnWilson.RankMatching.column_zero line 47
  12. lemma OAI.HahnWilson.RankMatching.columnSpace_eq_finite line 54
  13. lemma OAI.HahnWilson.RankMatching.columnSpace_finite line 65
  14. lemma OAI.HahnWilson.RankMatching.columnSpace_step line 70
  15. lemma OAI.HahnWilson.RankMatching.finrank_sup_singleton line 79
  16. def OAI.HahnWilson.RankMatching.intervalExtend line 92
  17. lemma OAI.HahnWilson.RankMatching.intervalExtend_injective line 97
  18. lemma OAI.HahnWilson.RankMatching.intervalExtend_col line 104
  19. lemma OAI.HahnWilson.RankMatching.columnSpace_eq_map line 115
  20. lemma OAI.HahnWilson.RankMatching.blockRank_eq_finrank line 128
  21. def OAI.HahnWilson.RankMatching.increment line 134
  22. lemma OAI.HahnWilson.RankMatching.blockRank_step line 137
  23. def OAI.HahnWilson.RankMatching.rowCut line 144
  24. lemma OAI.HahnWilson.RankMatching.rowCut_column line 149
  25. lemma OAI.HahnWilson.RankMatching.rowCut_columnSpace line 156
  26. lemma OAI.HahnWilson.RankMatching.increment_antitone line 164
  27. lemma OAI.HahnWilson.RankMatching.increment_le_one line 179
  28. lemma OAI.HahnWilson.RankMatching.weight_eq_increment_sub line 183
  29. lemma OAI.HahnWilson.RankMatching.weight_zero_or_one line 190
  30. lemma OAI.HahnWilson.RankMatching.matched_iff_increments line 199
  31. lemma OAI.HahnWilson.RankMatching.column_unique line 207
  32. def OAI.HahnWilson.RankMatching.reflected line 220
  33. lemma OAI.HahnWilson.RankMatching.triangular_reflected line 222
  34. def OAI.HahnWilson.RankMatching.negInterval line 227
  35. lemma OAI.HahnWilson.RankMatching.blockRank_reflected line 233
  36. lemma OAI.HahnWilson.RankMatching.weight_reflected line 240
  37. lemma OAI.HahnWilson.RankMatching.row_unique line 249
  38. lemma OAI.HahnWilson.RankMatching.blockRank_zero line 258
  39. lemma OAI.HahnWilson.RankMatching.increment_zero line 266
  40. lemma OAI.HahnWilson.RankMatching.sum_interval_difference line 270
  41. lemma OAI.HahnWilson.RankMatching.sum_interval_predecessor line 283
  42. lemma OAI.HahnWilson.RankMatching.sum_weights line 290
  43. lemma OAI.HahnWilson.RankMatching.rank_eq_count line 315
  44. theorem OAI.HahnWilson.RankMatching.rank_matching line 329
  45. lemma OAI.HahnWilson.RankMatching.increment_eq_zero_iff line 337
  46. lemma OAI.HahnWilson.RankMatching.increment_eq_one_iff line 341
  47. lemma OAI.HahnWilson.RankMatching.rowCut_map_columnSpace line 345
  48. lemma OAI.HahnWilson.RankMatching.columnSpace_supported line 352
  49. lemma OAI.HahnWilson.RankMatching.rowCut_injOn_of_equal_ranks line 363
  50. lemma OAI.HahnWilson.RankMatching.matched_oldUnmatched line 385
  51. lemma OAI.HahnWilson.RankMatching.block_eq_of_prior line 401
  52. lemma OAI.HahnWilson.RankMatching.oldUnmatched_of_prior line 414
  53. lemma OAI.HahnWilson.RankMatching.prior_columnSpace line 423
  54. lemma OAI.HahnWilson.RankMatching.prior_lower_column line 439
  55. lemma OAI.HahnWilson.RankMatching.oldUnmatched_lower_increment line 450
  56. lemma OAI.HahnWilson.RankMatching.exceptional_exists line 456
  57. def OAI.HahnWilson.RankMatching.cornerUpdate line 501
  58. lemma OAI.HahnWilson.RankMatching.triangular_cornerUpdate line 504
  59. lemma OAI.HahnWilson.RankMatching.prior_cornerUpdate line 511
  60. theorem OAI.HahnWilson.RankMatching.corner_rule line 517