OAI/Probability/ClassicalON/CoarseCodes.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ClassicalON.CoarseDirection line 9
  2. abbrev OAI.ClassicalON.CoarseCode line 10
  3. def OAI.ClassicalON.directionVector line 12
  4. def OAI.ClassicalON.codePosition line 13
  5. theorem OAI.ClassicalON.codePosition_zero line 16
  6. theorem OAI.ClassicalON.codePosition_succ line 19
  7. theorem OAI.ClassicalON.directionVector_surj line 23
  8. theorem OAI.ClassicalON.codePosition_exists line 31
  9. abbrev OAI.ClassicalON.SimpleCoarseCode line 40
  10. theorem OAI.ClassicalON.card_simpleCoarseCode line 42
  11. theorem OAI.ClassicalON.codeColor_exists line 47
  12. def OAI.ClassicalON.codeColor line 53
  13. theorem OAI.ClassicalON.codeColor_card line 56