OAI/Computability/PerfectCompleteness/Construction/ChildCallNumbering.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.ChildCallNumbering.Raw line 18
  2. instance OAI.PerfectCompleteness.ChildCallNumbering.rawFintype line 21
  3. instance OAI.PerfectCompleteness.ChildCallNumbering.rawNonempty line 25
  4. def OAI.PerfectCompleteness.ChildCallNumbering.equiv line 29
  5. theorem OAI.PerfectCompleteness.ChildCallNumbering.equiv_calls line 47
  6. theorem OAI.PerfectCompleteness.ChildCallNumbering.equiv_arrays line 52
  7. theorem OAI.PerfectCompleteness.ChildCallNumbering.equiv_symm_calls line 56
  8. theorem OAI.PerfectCompleteness.ChildCallNumbering.equiv_symm_arrays line 61
  9. def OAI.PerfectCompleteness.ChildCallNumbering.pullback line 66
  10. theorem OAI.PerfectCompleteness.ChildCallNumbering.pullback_calls line 84
  11. theorem OAI.PerfectCompleteness.ChildCallNumbering.pullback_arrays line 91
  12. theorem OAI.PerfectCompleteness.ChildCallNumbering.equiv_pullback line 97
  13. theorem OAI.PerfectCompleteness.ChildCallNumbering.pullback_cast line 106
  14. theorem OAI.PerfectCompleteness.ChildCallNumbering.uniform_equiv line 119
  15. theorem OAI.PerfectCompleteness.ChildCallNumbering.card_le line 127