OAI/Combinatorics/UniformKServer/RawMarks.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniformKServer.RawMarks.bits line 15
  2. def OAI.UniformKServer.RawMarks.empty line 16
  3. def OAI.UniformKServer.RawMarks.insert line 17
  4. def OAI.UniformKServer.RawMarks.card line 18
  5. def OAI.UniformKServer.RawMarks.complement line 19
  6. def OAI.UniformKServer.RawMarks.covers line 20
  7. def OAI.UniformKServer.RawMarks.pick line 21
  8. theorem OAI.UniformKServer.RawMarks.length_bits line 23
  9. theorem OAI.UniformKServer.RawMarks.empty_bits line 24
  10. theorem OAI.UniformKServer.RawMarks.insert_bits line 26
  11. theorem OAI.UniformKServer.RawMarks.card_bits line 39
  12. theorem OAI.UniformKServer.RawMarks.complement_bits line 41
  13. theorem OAI.UniformKServer.RawMarks.covers_bits line 44
  14. theorem OAI.UniformKServer.RawMarks.pick_bits line 48
  15. theorem OAI.UniformKServer.RawMarks.primitive_empty line 77
  16. theorem OAI.UniformKServer.RawMarks.primitive_insert line 81
  17. theorem OAI.UniformKServer.RawMarks.primitive_card line 83
  18. theorem OAI.UniformKServer.RawMarks.primitive_complement line 89
  19. theorem OAI.UniformKServer.RawMarks.primitive_covers line 91
  20. theorem OAI.UniformKServer.RawMarks.primitive_pick line 93