OAI/Computability/MinUncut/Estimates/UniformTransport.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncut.Preprocess.UEncoding.ofEquiv line 11
2. lemma OAI.MinUncut.Preprocess.UEncoding.map_to line 14
3. lemma OAI.MinUncut.Preprocess.UEncoding.map_from line 17
4. def OAI.MinUncut.Preprocess.UEncoding.pullback line 21
5. lemma OAI.MinUncut.Preprocess.UEncoding.Map.pullback line 24
6. lemma OAI.MinUncut.Preprocess.UEncoding.Map.first line 32
7. lemma OAI.MinUncut.Preprocess.UEncoding.Map.second line 35
8. lemma OAI.MinUncut.Preprocess.UEncoding.Map.specialize line 39
9. def OAI.MinUncut.Preprocess.UEncoding.sum line 49
10. lemma OAI.MinUncut.Preprocess.UEncoding.sum_code_inl line 53
11. lemma OAI.MinUncut.Preprocess.UEncoding.sum_code_inr line 56
12. lemma OAI.MinUncut.Preprocess.UEncoding.map_inl line 58
13. lemma OAI.MinUncut.Preprocess.UEncoding.map_inr line 61
14. lemma OAI.MinUncut.Preprocess.UEncoding.map_case line 66