OAI/Computability/PerfectCompleteness/Foundations/WholeCutCallsLemmas.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.WholeCutCalls.Index line 16
  2. instance OAI.PerfectCompleteness.WholeCutCalls.indexFintype line 22
  3. def OAI.PerfectCompleteness.WholeCutCalls.directRow line 32
  4. theorem OAI.PerfectCompleteness.WholeCutCalls.directRow_injective line 37
  5. theorem OAI.PerfectCompleteness.WholeCutCalls.root_ne_lower line 45
  6. theorem OAI.PerfectCompleteness.WholeCutCalls.direction_card line 53
  7. theorem OAI.PerfectCompleteness.WholeCutCalls.card_refl line 60
  8. theorem OAI.PerfectCompleteness.WholeCutCalls.card_step line 64
  9. theorem OAI.PerfectCompleteness.WholeCutCalls.card_eq_formula line 74
  10. def OAI.PerfectCompleteness.OriginalCutCalls.Index line 99
  11. instance OAI.PerfectCompleteness.OriginalCutCalls.indexFintype line 105
  12. def OAI.PerfectCompleteness.OriginalCutCalls.ownBucket line 115
  13. theorem OAI.PerfectCompleteness.OriginalCutCalls.ownBucket_injective line 120
  14. def OAI.PerfectCompleteness.OriginalCutCalls.rootCall line 128
  15. def OAI.PerfectCompleteness.OriginalCutCalls.lowerCall line 132
  16. theorem OAI.PerfectCompleteness.OriginalCutCalls.rootCall_injective line 135
  17. theorem OAI.PerfectCompleteness.OriginalCutCalls.lowerCall_injective line 140
  18. theorem OAI.PerfectCompleteness.OriginalCutCalls.root_ne_lower line 145
  19. theorem OAI.PerfectCompleteness.OriginalCutCalls.root_ne_ownBucket line 153
  20. theorem OAI.PerfectCompleteness.OriginalCutCalls.rootCall_mk_eq_iff line 160
  21. theorem OAI.PerfectCompleteness.OriginalCutCalls.card_refl line 172
  22. theorem OAI.PerfectCompleteness.OriginalCutCalls.card_step line 176
  23. theorem OAI.PerfectCompleteness.OriginalCutCalls.card_eq_formula line 186
  24. def OAI.PerfectCompleteness.OriginalCutCalls.count line 197
  25. theorem OAI.PerfectCompleteness.OriginalCutCalls.card_eq_count line 202
  26. theorem OAI.PerfectCompleteness.OriginalCutCalls.card_branch_independent line 206