OAI/Computability/PerfectCompleteness/Construction/CutChildGrouping.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.CutChildGrouping.F2 line 14
  2. abbrev OAI.PerfectCompleteness.CutChildGrouping.Child line 22
  3. instance OAI.PerfectCompleteness.CutChildGrouping.childFintype line 25
  4. abbrev OAI.PerfectCompleteness.CutChildGrouping.Raw line 28
  5. abbrev OAI.PerfectCompleteness.CutChildGrouping.Assembled line 30
  6. instance OAI.PerfectCompleteness.CutChildGrouping.assembledFintype line 33
  7. def OAI.PerfectCompleteness.CutChildGrouping.rawLaw line 35
  8. def OAI.PerfectCompleteness.CutChildGrouping.assemble line 38
  9. theorem OAI.PerfectCompleteness.CutChildGrouping.assemble_calls line 56
  10. theorem OAI.PerfectCompleteness.CutChildGrouping.assemble_arrays line 62
  11. theorem OAI.PerfectCompleteness.CutChildGrouping.assemble_surjective line 66
  12. theorem OAI.PerfectCompleteness.CutChildGrouping.assemble_law line 79
  13. theorem OAI.PerfectCompleteness.CutChildGrouping.projected_child_type line 87