OAI/InformationTheory/Entanglement/CombinatorialOrder.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.FiniteConstruction.baseLinearOrder line 10
  2. instance OAI.FiniteConstruction.(instance at line 16) line 16
  3. instance OAI.FiniteConstruction.(instance at line 17) line 17
  4. instance OAI.FiniteConstruction.questionLinearOrder line 19
  5. instance OAI.FiniteConstruction.(instance at line 25) line 25
  6. instance OAI.FiniteConstruction.(instance at line 26) line 26
  7. abbrev OAI.FiniteConstruction.Eight line 27
  8. instance OAI.FiniteConstruction.eightLinearOrder line 28
  9. instance OAI.FiniteConstruction.(instance at line 34) line 34
  10. instance OAI.FiniteConstruction.(instance at line 35) line 35
  11. lemma OAI.FiniteConstruction.eight_card line 36
  12. def OAI.FiniteConstruction.six line 39
  13. lemma OAI.FiniteConstruction.six_mem line 41
  14. lemma OAI.FiniteConstruction.six_injective line 43
  15. def OAI.FiniteConstruction.OrthogonalEight line 46
  16. def OAI.FiniteConstruction.contextAt line 49
  17. lemma OAI.FiniteConstruction.contextAt_six line 54
  18. lemma OAI.FiniteConstruction.contextAt_some line 60
  19. abbrev OAI.FiniteConstruction.OutputCoordinate line 69
  20. abbrev OAI.FiniteConstruction.Label line 70
  21. lemma OAI.FiniteConstruction.four_card line 71
  22. lemma OAI.FiniteConstruction.outcome_card line 72
  23. lemma OAI.FiniteConstruction.card_arrow_eq line 74
  24. lemma OAI.FiniteConstruction.card_pair_eq line 77
  25. lemma OAI.FiniteConstruction.output_card line 80
  26. lemma OAI.FiniteConstruction.outcomeString_card line 83
  27. lemma OAI.FiniteConstruction.label_card line 86
  28. instance OAI.FiniteConstruction.fourLinearOrder line 90
  29. instance OAI.FiniteConstruction.(instance at line 92) line 92
  30. instance OAI.FiniteConstruction.(instance at line 93) line 93
  31. instance OAI.FiniteConstruction.eightWellFounded line 94
  32. instance OAI.FiniteConstruction.outputLinearOrder line 97
  33. instance OAI.FiniteConstruction.labelLinearOrder line 99
  34. def OAI.FiniteConstruction.orderedEnumeration line 102
  35. def OAI.FiniteConstruction.outputEnumeration line 109
  36. def OAI.FiniteConstruction.labelEnumeration line 110