MIL/C04_Sets_and_Functions/S01_Sets.lean

GitHub source file

42 declarations, 12 contain sorry, 0 declared as axioms

Imports (3)
Imported by 1 file
  1. example (example at line 10) line 10 source
  2. example (example at line 17) line 17 source
  3. example (example at line 22) line 22 source
  4. example (example at line 26) line 26 source
  5. example (example at line 29) line 29 source
  6. example (example at line 41) line 41 source
  7. example (example at line 46) sorry line 46 source
  8. example (example at line 48) line 48 source
  9. example (example at line 61) line 61 source
  10. example (example at line 66) sorry line 66 source
  11. example (example at line 68) line 68 source
  12. example (example at line 75) line 75 source
  13. example (example at line 78) line 78 source
  14. example (example at line 80) line 80 source
  15. example (example at line 85) sorry line 85 source
  16. example (example at line 87) sorry line 87 source
  17. example (example at line 90) sorry line 90 source
  18. example (example at line 93) sorry line 93 source
  19. example (example at line 96) sorry line 96 source
  20. def evens line 99 source

    no axioms what this means

    Statement uses: Set, Nat

    Proof uses: setOf, Even

    1 instances, coercions and auxiliary constants left out.

  21. def odds line 102 source

    no axioms what this means

    Statement uses: Set, Nat

    Proof uses: setOf, Not, Even

    1 instances, coercions and auxiliary constants left out.

    Tactic trace: 42 steps

    Open to load the checked before-and-after goal states.

  22. example (example at line 105) line 105 source
  23. example (example at line 111) line 111 source
  24. example (example at line 114) line 114 source
  25. example (example at line 117) sorry line 117 source
  26. example (example at line 124) line 124 source
  27. example (example at line 127) line 127 source
  28. example (example at line 131) line 131 source
  29. example (example at line 140) line 140 source
  30. example (example at line 146) line 146 source
  31. example (example at line 153) sorry line 153 source
  32. example (example at line 156) sorry line 156 source
  33. example (example at line 170) line 170 source
  34. example (example at line 179) line 179 source
  35. example (example at line 195) sorry line 195 source
  36. def primes line 198 source

    standard axioms: propext what this means

    Statement uses: Set, Nat

    Proof uses: setOf, Nat.Prime

    Also declared: MIL/C04_Sets_and_Functions/solutions/Solutions_S01_Sets.lean:139 (same declaration text).

    Tactic trace: 16 steps

    Open to load the checked before-and-after goal states.

  37. example (example at line 201) line 201 source
  38. example (example at line 206) line 206 source
  39. example (example at line 210) line 210 source
  40. example (example at line 216) sorry line 216 source
  41. example (example at line 227) line 227 source
  42. example (example at line 232) line 232 source