OAI/Combinatorics/SnakyCertificate/Lists.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SnakyCertificate.Check.Key line 7
  2. def OAI.SnakyCertificate.Check.mergeFuel line 9
  3. theorem OAI.SnakyCertificate.Check.mem_mergeFuel line 18
  4. def OAI.SnakyCertificate.Check.mergeUnion line 36
  5. theorem OAI.SnakyCertificate.Check.mem_mergeUnion line 39
  6. theorem OAI.SnakyCertificate.Check.toFinset_mergeUnion line 43
  7. structure OAI.SnakyCertificate.Check.ListRow line 47
  8. def OAI.SnakyCertificate.Check.denote line 53
  9. def OAI.SnakyCertificate.Check.keyPlace line 55
  10. def OAI.SnakyCertificate.Check.sortFuel line 58
  11. theorem OAI.SnakyCertificate.Check.mem_sortFuel line 65
  12. def OAI.SnakyCertificate.Check.sorted line 75
  13. def OAI.SnakyCertificate.Check.place line 77
  14. def OAI.SnakyCertificate.Check.unions line 80
  15. def OAI.SnakyCertificate.Check.common line 82
  16. def OAI.SnakyCertificate.Check.fork line 87
  17. theorem OAI.SnakyCertificate.Check.toFinset_sorted line 93
  18. theorem OAI.SnakyCertificate.Check.denote_place line 96
  19. theorem OAI.SnakyCertificate.Check.toFinset_unions line 104
  20. theorem OAI.SnakyCertificate.Check.toFinset_inter_cell line 110
  21. theorem OAI.SnakyCertificate.Check.toFinset_inters line 114
  22. theorem OAI.SnakyCertificate.Check.toFinset_common line 120
  23. theorem OAI.SnakyCertificate.Check.denote_fork line 126