OAI/Computability/PerfectCompleteness/Foundations/TerminalCalls.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.TerminalCalls.TerminalIndex line 17
  2. instance OAI.PerfectCompleteness.TerminalCalls.terminalIndexFintype line 22
  3. instance OAI.PerfectCompleteness.TerminalCalls.terminalIndexDecidableEq line 31
  4. def OAI.PerfectCompleteness.TerminalCalls.drawIndex line 40
  5. theorem OAI.PerfectCompleteness.TerminalCalls.drawIndex_refl line 45
  6. theorem OAI.PerfectCompleteness.TerminalCalls.drawIndex_step line 49
  7. theorem OAI.PerfectCompleteness.TerminalCalls.drawIndex_injective line 54
  8. def OAI.PerfectCompleteness.TerminalCalls.terminalEmbedding line 67
  9. def OAI.PerfectCompleteness.TerminalCalls.IsTerminal line 71
  10. theorem OAI.PerfectCompleteness.TerminalCalls.isTerminal_refl line 79
  11. theorem OAI.PerfectCompleteness.TerminalCalls.not_isTerminal_ordinary line 83
  12. theorem OAI.PerfectCompleteness.TerminalCalls.isTerminal_recursive line 87
  13. theorem OAI.PerfectCompleteness.TerminalCalls.isTerminal_iff_exists line 92
  14. theorem OAI.PerfectCompleteness.TerminalCalls.isTerminal_drawIndex line 124
  15. def OAI.PerfectCompleteness.TerminalCalls.terminalSubtypeEquiv line 129
  16. theorem OAI.PerfectCompleteness.TerminalCalls.terminalSubtypeEquiv_apply line 138
  17. theorem OAI.PerfectCompleteness.TerminalCalls.card_refl line 142
  18. theorem OAI.PerfectCompleteness.TerminalCalls.card_step line 147
  19. theorem OAI.PerfectCompleteness.TerminalCalls.card_eq_prod line 154
  20. theorem OAI.PerfectCompleteness.TerminalCalls.drawSpace_eq_terminal line 162
  21. def OAI.PerfectCompleteness.TerminalCalls.terminalSpaceEquiv line 173