OAI/Computability/PerfectCompleteness/Foundations/RecursiveSpaces.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.RecursiveSpaces.Slots line 14
  2. instance OAI.PerfectCompleteness.RecursiveSpaces.slotsFintype line 18
  3. instance OAI.PerfectCompleteness.RecursiveSpaces.slotsDecidableEq line 25
  4. abbrev OAI.PerfectCompleteness.RecursiveSpaces.Assignment line 35
  5. abbrev OAI.PerfectCompleteness.RecursiveSpaces.childFamily line 37
  6. def OAI.PerfectCompleteness.RecursiveSpaces.childRestriction line 40
  7. theorem OAI.PerfectCompleteness.RecursiveSpaces.assignment_finite line 43
  8. theorem OAI.PerfectCompleteness.RecursiveSpaces.childRestriction_surjective line 47
  9. def OAI.PerfectCompleteness.RecursiveSpaces.space line 58
  10. theorem OAI.PerfectCompleteness.RecursiveSpaces.space_zero line 67
  11. theorem OAI.PerfectCompleteness.RecursiveSpaces.space_succ line 70
  12. theorem OAI.PerfectCompleteness.RecursiveSpaces.space_finite line 74
  13. theorem OAI.PerfectCompleteness.RecursiveSpaces.one_mem_space line 78
  14. theorem OAI.PerfectCompleteness.RecursiveSpaces.space_le_squareSpace line 94
  15. theorem OAI.PerfectCompleteness.RecursiveSpaces.one_mem_space_square line 99
  16. theorem OAI.PerfectCompleteness.RecursiveSpaces.child_square_le_space line 104
  17. theorem OAI.PerfectCompleteness.RecursiveSpaces.child_le_space line 110
  18. theorem OAI.PerfectCompleteness.RecursiveSpaces.child_pullback_injective line 117
  19. def OAI.PerfectCompleteness.RecursiveSpaces.project line 122
  20. theorem OAI.PerfectCompleteness.RecursiveSpaces.project_apply line 126
  21. theorem OAI.PerfectCompleteness.RecursiveSpaces.project_surjective line 130
  22. theorem OAI.PerfectCompleteness.RecursiveSpaces.project_child line 135
  23. theorem OAI.PerfectCompleteness.RecursiveSpaces.space_project_le line 141
  24. theorem OAI.PerfectCompleteness.RecursiveSpaces.squareSpace_project_le line 161
  25. def OAI.PerfectCompleteness.RecursiveSpaces.spacePullback line 167
  26. theorem OAI.PerfectCompleteness.RecursiveSpaces.spacePullback_apply line 174
  27. theorem OAI.PerfectCompleteness.RecursiveSpaces.spacePullback_injective line 178