OAI/Combinatorics/ContingencyTables/Counting/CompanionStoredShape.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Height and shape invariants for chronological stored values

  1. def OAI.ContingencyTables.CompanionStoredSize.StoredShape line 10
  2. lemma OAI.ContingencyTables.CompanionStoredSize.height_mono line 13
  3. lemma OAI.ContingencyTables.CompanionStoredSize.shape_mono line 16
  4. lemma OAI.ContingencyTables.CompanionStoredSize.shape_of_weight line 19
  5. lemma OAI.ContingencyTables.CompanionStoredSize.height_of_weight line 24
  6. lemma OAI.ContingencyTables.CompanionStoredSize.weight_of_bounds line 30
  7. lemma OAI.ContingencyTables.CompanionStoredSize.next_shape line 46