OAI/Combinatorics/ContingencyTables/Transport/RowMajorEnumeration.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Increasing enumeration of the actual finite small cells

  1. abbrev OAI.ContingencyTables.RowMajorEnumeration.LexCells line 18
  2. def OAI.ContingencyTables.RowMajorEnumeration.lexCellEquiv line 21
  3. def OAI.ContingencyTables.RowMajorEnumeration.enumeration line 27
  4. lemma OAI.ContingencyTables.RowMajorEnumeration.enumeration_before_iff line 31
  5. def OAI.ContingencyTables.RowMajorEnumeration.earlierIndexEquiv line 43
  6. def OAI.ContingencyTables.RowMajorEnumeration.laterIndexEquiv line 53
  7. def OAI.ContingencyTables.RowMajorEnumeration.earlierFinEquiv line 63
  8. def OAI.ContingencyTables.RowMajorEnumeration.laterFinEquiv line 69
  9. def OAI.ContingencyTables.RowMajorEnumeration.earlierEnumeration line 77
  10. def OAI.ContingencyTables.RowMajorEnumeration.laterEnumeration line 81
  11. lemma OAI.ContingencyTables.RowMajorEnumeration.small_card_le_dimension line 87