MIL/C04_Sets_and_Functions/solutions/Solutions_S01_Sets.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Imports (3)
  1. example (example at line 10) line 10 source
  2. example (example at line 15) line 15 source
  3. example (example at line 24) line 24 source
  4. example (example at line 28) line 28 source
  5. example (example at line 35) line 35 source
  6. example (example at line 40) line 40 source
  7. example (example at line 56) line 56 source
  8. example (example at line 79) line 79 source
  9. example (example at line 97) line 97 source
  10. example (example at line 103) line 103 source
  11. example (example at line 118) line 118 source
  12. def primes line 139 source

    standard axioms: propext what this means

    Statement uses: Set, Nat

    Proof uses: setOf, Nat.Prime

    Also declared: MIL/C04_Sets_and_Functions/S01_Sets.lean:198 (same declaration text).

    Tactic trace: 5 steps

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

  13. example (example at line 142) line 142 source