OAI/Combinatorics/ThinTrees/Pencil/FiniteFamilies.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Finite families.

  1. instance OAI.CurrentKS.Realization.poly_dite line 15
  2. def OAI.CurrentKS.Realization.indexedCode line 31
  3. def OAI.CurrentKS.Realization.indexedFirst line 34
  4. def OAI.CurrentKS.Realization.indexedIndex line 38
  5. instance OAI.CurrentKS.Realization.poly_indexedFirst line 42
  6. instance OAI.CurrentKS.Realization.poly_indexedIndex line 44
  7. def OAI.CurrentKS.Realization.Realizes.tabulateIndexed line 47
  8. instance OAI.CurrentKS.Realization.poly_tabulateIndexed line 52
  9. def OAI.CurrentKS.Realization.sumEquiv line 60
  10. def OAI.CurrentKS.Realization.sumLeft line 64
  11. def OAI.CurrentKS.Realization.sumRight line 67
  12. lemma OAI.CurrentKS.Realization.sumLeft_code line 71
  13. lemma OAI.CurrentKS.Realization.sumRight_index line 78
  14. def OAI.CurrentKS.Realization.indexedSumTest line 87
  15. instance OAI.CurrentKS.Realization.poly_indexedSumTest line 97
  16. def OAI.CurrentKS.Realization.indexedSumRight line 101
  17. instance OAI.CurrentKS.Realization.poly_indexedSumRight line 116
  18. def OAI.CurrentKS.Realization.Realizes.sumCases line 120
  19. instance OAI.CurrentKS.Realization.poly_sumCases line 131
  20. def OAI.CurrentKS.Realization.prodEquiv line 137
  21. def OAI.CurrentKS.Realization.splitProduct line 141
  22. instance OAI.CurrentKS.Realization.poly_splitProduct line 159
  23. def OAI.CurrentKS.Realization.Realizes.prodCases line 163
  24. instance OAI.CurrentKS.Realization.poly_prodCases line 169
  25. def OAI.CurrentKS.Realization.indexedProductLeft line 175
  26. instance OAI.CurrentKS.Realization.poly_indexedProductLeft line 180
  27. def OAI.CurrentKS.Realization.indexedProductRight line 184
  28. instance OAI.CurrentKS.Realization.poly_indexedProductRight line 192
  29. def OAI.CurrentKS.Realization.Realizes.not line 196
  30. instance OAI.CurrentKS.Realization.poly_not line 200
  31. def OAI.CurrentKS.Realization.Realizes.and line 204
  32. instance OAI.CurrentKS.Realization.poly_and line 209
  33. def OAI.CurrentKS.Realization.Realizes.finEq line 214
  34. instance OAI.CurrentKS.Realization.poly_finEq line 219