OAI/Combinatorics/Chromatic/Walls/Pack.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ElementaryPositivity.PackConvolution.Pack line 13
  2. abbrev OAI.ElementaryPositivity.PackConvolution.Cut line 14
  3. def OAI.ElementaryPositivity.PackConvolution.left line 16
  4. def OAI.ElementaryPositivity.PackConvolution.right line 17
  5. def OAI.ElementaryPositivity.PackConvolution.kernel line 19
  6. lemma OAI.ElementaryPositivity.PackConvolution.kernel_union_left line 22
  7. lemma OAI.ElementaryPositivity.PackConvolution.kernel_union_right line 26
  8. abbrev OAI.ElementaryPositivity.PackConvolution.LeftIndex line 33
  9. abbrev OAI.ElementaryPositivity.PackConvolution.RightIndex line 34
  10. def OAI.ElementaryPositivity.PackConvolution.distribute line 36
  11. def OAI.ElementaryPositivity.PackConvolution.rebracket line 43
  12. def OAI.ElementaryPositivity.PackConvolution.shuffle line 47
  13. lemma OAI.ElementaryPositivity.PackConvolution.shuffle_assoc line 51
  14. abbrev OAI.ElementaryPositivity.PackEnumeration.Split line 84
  15. def OAI.ElementaryPositivity.PackEnumeration.embedding line 87
  16. lemma OAI.ElementaryPositivity.PackEnumeration.map_univ line 91
  17. def OAI.ElementaryPositivity.PackEnumeration.split line 101
  18. lemma OAI.ElementaryPositivity.PackEnumeration.split_injective line 106
  19. lemma OAI.ElementaryPositivity.PackEnumeration.split_right_unique line 111
  20. lemma OAI.ElementaryPositivity.PackEnumeration.split_surjective line 134
  21. def OAI.ElementaryPositivity.PackEnumeration.splitEquiv line 150
  22. lemma OAI.ElementaryPositivity.PackEnumeration.splitEquiv_left line 153
  23. lemma OAI.ElementaryPositivity.PackEnumeration.splitEquiv_right line 155
  24. def OAI.ElementaryPositivity.PackEnumeration.sizedSplitEquiv line 158
  25. def OAI.ElementaryPositivity.PackEnumeration.mapEquiv line 162
  26. lemma OAI.ElementaryPositivity.PackEnumeration.mapEquiv_apply line 173