OAI/Combinatorics/UniformKServer/RawFilter.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniformKServer.RawFilter.E line 12
  2. abbrev OAI.UniformKServer.RawFilter.F line 13
  3. def OAI.UniformKServer.RawFilter.cover line 15
  4. def OAI.UniformKServer.RawFilter.allCover line 16
  5. def OAI.UniformKServer.RawFilter.expand line 17
  6. def OAI.UniformKServer.RawFilter.births line 20
  7. def OAI.UniformKServer.RawFilter.step line 22
  8. def OAI.UniformKServer.RawFilter.entry line 25
  9. def OAI.UniformKServer.RawFilter.state line 26
  10. theorem OAI.UniformKServer.RawFilter.cover_entry line 29
  11. theorem OAI.UniformKServer.RawFilter.allCover_state line 34
  12. theorem OAI.UniformKServer.RawFilter.expand_entry line 39
  13. theorem OAI.UniformKServer.RawFilter.births_entry line 55
  14. theorem OAI.UniformKServer.RawFilter.step_state line 61
  15. theorem OAI.UniformKServer.RawFilter.primitive_cover line 72
  16. theorem OAI.UniformKServer.RawFilter.primitive_allCover line 76
  17. theorem OAI.UniformKServer.RawFilter.primitive_expand line 78
  18. theorem OAI.UniformKServer.RawFilter.primitive_births line 86
  19. theorem OAI.UniformKServer.RawFilter.primitive_step line 94