MIL/C04_Sets_and_Functions/S02_Functions.lean

GitHub source file

36 declarations, 27 contain sorry, 0 declared as axioms

Imports (4)
Imported by 1 file
  1. example (example at line 16) line 16 source
  2. example (example at line 20) line 20 source
  3. example (example at line 31) line 31 source
  4. example (example at line 36) sorry line 36 source
  5. example (example at line 39) sorry line 39 source
  6. example (example at line 42) sorry line 42 source
  7. example (example at line 45) sorry line 45 source
  8. example (example at line 48) sorry line 48 source
  9. example (example at line 51) sorry line 51 source
  10. example (example at line 54) sorry line 54 source
  11. example (example at line 57) sorry line 57 source
  12. example (example at line 60) sorry line 60 source
  13. example (example at line 63) sorry line 63 source
  14. example (example at line 66) sorry line 66 source
  15. example (example at line 69) sorry line 69 source
  16. example (example at line 72) sorry line 72 source
  17. example (example at line 75) sorry line 75 source
  18. example (example at line 78) sorry line 78 source
  19. example (example at line 83) sorry line 83 source
  20. example (example at line 86) sorry line 86 source
  21. example (example at line 89) sorry line 89 source
  22. example (example at line 92) sorry line 92 source
  23. example (example at line 95) sorry line 95 source
  24. example (example at line 98) line 98 source
  25. example (example at line 107) line 107 source
  26. example (example at line 115) line 115 source
  27. example (example at line 123) sorry line 123 source
  28. example (example at line 126) sorry line 126 source
  29. example (example at line 129) sorry line 129 source
  30. example (example at line 132) sorry line 132 source
  31. example (example at line 146) line 146 source
  32. def inverse line 153 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Inhabited

    Proof uses: dite, Exists, Eq, Classical.propDecidable, Classical.choose, Not, Inhabited.default

    Also declared: MIL/C04_Sets_and_Functions/solutions/Solutions_S02_Functions.lean:196 (same declaration text).

  33. theorem inverse_spec line 156 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Inhabited, Exists, Eq, inverse

    Proof uses: Eq.mpr, dite, Classical.propDecidable, Classical.choose, Not, Inhabited.default, id, congrArg, inverse.eq_1, dif_pos, Classical.choose_spec

    Also declared: MIL/C04_Sets_and_Functions/solutions/Solutions_S02_Functions.lean:199 (same declaration text).

    Tactic trace: 2 steps

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

  34. example (example at line 164) sorry line 164 source
  35. example (example at line 167) sorry line 167 source
  36. theorem Cantor sorry line 176 source

    depends on sorry what this means

    Statement uses: Set, Not, Function.Surjective

    Proof uses: setOf, Membership.mem, Eq, Exists, False, Eq.mp, congrArg, False.elim, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    3 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C04_Sets_and_Functions/solutions/Solutions_S02_Functions.lean:237 (same statement text; different proof or body). Qualify references as Cantor@path.

    Tactic trace: 13 steps

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