OAI/Probability/SwitchChain/ForcedColumns.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem315.ForcedColumns.MatrixSpace line 12
  2. abbrev OAI.Problem315.ForcedColumns.One line 15
  3. abbrev OAI.Problem315.ForcedColumns.Two line 16
  4. lemma OAI.Problem315.ForcedColumns.column_zero line 18
  5. lemma OAI.Problem315.ForcedColumns.column_three line 23
  6. def OAI.Problem315.ForcedColumns.restrict line 28
  7. def OAI.Problem315.ForcedColumns.extend line 34
  8. theorem OAI.Problem315.ForcedColumns.restrict_extend line 50
  9. theorem OAI.Problem315.ForcedColumns.extend_restrict line 60
  10. def OAI.Problem315.ForcedColumns.matrixEquiv line 78
  11. theorem OAI.Problem315.ForcedColumns.row_eq_iff line 85
  12. def OAI.Problem315.ForcedColumns.offset line 110
  13. theorem OAI.Problem315.ForcedColumns.row_sum line 112
  14. theorem OAI.Problem315.ForcedColumns.offset_le_row_sum line 148
  15. def OAI.Problem315.ForcedColumns.fixedMarginsEquiv line 153
  16. abbrev OAI.Problem315.ForcedColumns.FullMargins line 172
  17. def OAI.Problem315.ForcedColumns.nestEquiv line 176
  18. theorem OAI.Problem315.ForcedColumns.bounds_of_nonempty line 183
  19. abbrev OAI.Problem315.ForcedColumns.Colorings line 201
  20. def OAI.Problem315.ForcedColumns.coloringEquiv line 206
  21. theorem OAI.Problem315.ForcedColumns.coloring_row_eq_iff line 214