OAI/Combinatorics/SumProduct/Alignment/DenseBoolean01.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DenseBooleanCubes.PositiveCube line 23
  2. lemma OAI.DenseBooleanCubes.dense_shift line 28
  3. lemma OAI.DenseBooleanCubes.cube_of_shift line 78
  4. theorem OAI.DenseBooleanCubes.dense_positive_cube line 93
  5. def OAI.DenseBooleanCubes.blockResidues line 128
  6. lemma OAI.DenseBooleanCubes.blockResidues_subset line 131
  7. lemma OAI.DenseBooleanCubes.blockResidues_card line 137
  8. lemma OAI.DenseBooleanCubes.mem_from_residue line 151
  9. lemma OAI.DenseBooleanCubes.dense_block line 158
  10. theorem OAI.DenseBooleanCubes.dense_bounded_positive_cube line 176
  11. def OAI.DenseBooleanCubes.CubeSubspace.offset line 203
  12. def OAI.DenseBooleanCubes.CubeSubspace.weight line 205
  13. lemma OAI.DenseBooleanCubes.CubeSubspace.value line 207
  14. lemma OAI.DenseBooleanCubes.CubeSubspace.weight_pos line 222
  15. lemma OAI.DenseBooleanCubes.CubeSubspace.weight_le line 231
  16. theorem OAI.DenseBooleanCubes.colored_subcube line 242
  17. theorem OAI.DenseBooleanCubes.dense_colored_bounded_cube line 247