MIL/C02_Basics/S03_Using_Theorems_and_Lemmas.lean

GitHub source file

19 declarations, 5 contain sorry, 0 declared as axioms

1. example (example at line 21) line 21 source
2. example (example at line 26) line 26 source
3. example (example at line 30) line 30 source
4. example (example at line 33) line 33 source
5. example (example at line 36) line 36 source
6. example (example at line 46) sorry line 46 source

   Source comment

   Try this.

   example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := by
   …

7. example (example at line 49) line 49 source
8. example (example at line 54) line 54 source
9. example (example at line 59) line 59 source
10. example (example at line 79) line 79 source
11. example (example at line 83) line 83 source
12. example (example at line 89) sorry line 89 source
13. example (example at line 91) line 91 source
14. example (example at line 93) sorry line 93 source
15. example (example at line 98) line 98 source
16. example (example at line 102) sorry line 102 source
17. example (example at line 105) line 105 source
18. example (example at line 116) line 116 source
19. example (example at line 123) sorry line 123 source