OAI/Computability/MinUncut/Estimates/UniformRestrict.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncut.Preprocess.UEncoding.goodCodes line 11
  2. lemma OAI.MinUncut.Preprocess.UEncoding.goodCodes_nodup line 13
  3. lemma OAI.MinUncut.Preprocess.UEncoding.mem_goodCodes line 15
  4. lemma OAI.MinUncut.Preprocess.UEncoding.original_mem_goodCodes line 19
  5. lemma OAI.MinUncut.Preprocess.UEncoding.computable_goodCodes line 25
  6. def OAI.MinUncut.Preprocess.UEncoding.restrictEquiv line 54
  7. def OAI.MinUncut.Preprocess.UEncoding.restrict line 62
  8. lemma OAI.MinUncut.Preprocess.UEncoding.restrict_code line 68
  9. lemma OAI.MinUncut.Preprocess.UEncoding.map_restrict_val line 72
  10. lemma OAI.MinUncut.Preprocess.UEncoding.map_restrict_mk line 82
  11. def OAI.MinUncut.Preprocess.UEncoding.Out line 99
  12. lemma OAI.MinUncut.Preprocess.UEncoding.Out.ofEq line 101
  13. lemma OAI.MinUncut.Preprocess.UEncoding.out_const line 105
  14. lemma OAI.MinUncut.Preprocess.UEncoding.out_code line 107
  15. lemma OAI.MinUncut.Preprocess.UEncoding.Out.comp line 109
  16. lemma OAI.MinUncut.Preprocess.UEncoding.Out.map line 116
  17. lemma OAI.MinUncut.Preprocess.UEncoding.Out.map₂ line 120
  18. lemma OAI.MinUncut.Preprocess.UEncoding.Out.pair line 126
  19. lemma OAI.MinUncut.Preprocess.UEncoding.Out.first line 129
  20. lemma OAI.MinUncut.Preprocess.UEncoding.Out.second line 131
  21. lemma OAI.MinUncut.Preprocess.UEncoding.out_list line 134
  22. lemma OAI.MinUncut.Preprocess.UEncoding.Out.enumerate line 157
  23. lemma OAI.MinUncut.Preprocess.UEncoding.fixed_out line 163
  24. lemma OAI.MinUncut.Preprocess.UEncoding.Map.out line 172
  25. lemma OAI.MinUncut.Preprocess.UEncoding.Out.toBool line 174
  26. lemma OAI.MinUncut.Preprocess.UEncoding.Out.toFin line 181
  27. lemma OAI.MinUncut.Preprocess.UEncoding.Out.cond line 184