OAI/Computability/PerfectCompleteness/Construction/TreeSourceSpaces.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.TreeSourceSpaces.F2 line 13
  2. instance OAI.PerfectCompleteness.TreeSourceSpaces.slotDomainFintype line 17
  3. abbrev OAI.PerfectCompleteness.TreeSourceSpaces.LeafDomain line 23
  4. abbrev OAI.PerfectCompleteness.TreeSourceSpaces.Domain line 26
  5. abbrev OAI.PerfectCompleteness.TreeSourceSpaces.H line 29
  6. theorem OAI.PerfectCompleteness.TreeSourceSpaces.domain_nonempty line 33
  7. theorem OAI.PerfectCompleteness.TreeSourceSpaces.domain_finite line 37
  8. theorem OAI.PerfectCompleteness.TreeSourceSpaces.H_finite line 41
  9. theorem OAI.PerfectCompleteness.TreeSourceSpaces.one_mem_H line 45
  10. theorem OAI.PerfectCompleteness.TreeSourceSpaces.H_le_squareSpace line 49
  11. theorem OAI.PerfectCompleteness.TreeSourceSpaces.one_mem_squareSpace line 53
  12. def OAI.PerfectCompleteness.TreeSourceSpaces.sourceProjection line 58
  13. theorem OAI.PerfectCompleteness.TreeSourceSpaces.sourceProjection_apply line 63
  14. theorem OAI.PerfectCompleteness.TreeSourceSpaces.sourceProjection_surjective line 69
  15. theorem OAI.PerfectCompleteness.TreeSourceSpaces.H_pullback_le line 76
  16. theorem OAI.PerfectCompleteness.TreeSourceSpaces.squareSpace_pullback_le line 82
  17. def OAI.PerfectCompleteness.TreeSourceSpaces.HPullback line 90
  18. theorem OAI.PerfectCompleteness.TreeSourceSpaces.HPullback_apply line 95
  19. theorem OAI.PerfectCompleteness.TreeSourceSpaces.HPullback_injective line 101
  20. abbrev OAI.PerfectCompleteness.TreeSourceSpaces.childSlots line 109
  21. def OAI.PerfectCompleteness.TreeSourceSpaces.restrictChild line 113
  22. theorem OAI.PerfectCompleteness.TreeSourceSpaces.child_square_le_H line 117
  23. theorem OAI.PerfectCompleteness.TreeSourceSpaces.child_H_le_H line 123
  24. theorem OAI.PerfectCompleteness.TreeSourceSpaces.restrictChild_surjective line 128
  25. def OAI.PerfectCompleteness.TreeSourceSpaces.flatSlots line 132
  26. def OAI.PerfectCompleteness.TreeSourceSpaces.flattenAssignment line 135
  27. theorem OAI.PerfectCompleteness.TreeSourceSpaces.flattenAssignment_projection line 147