MIL/C04_Sets_and_Functions/solutions/Solutions_S02_Functions.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned Mathematics in Lean documentation, Pinned Mathematics in Lean textbook

31 declarations, 0 contain sorry, 0 declared as axioms

Imports (4)
  1. example (example at line 16) line 16 source
  2. example (example at line 26) line 26 source
  3. example (example at line 31) line 31 source
  4. example (example at line 35) line 35 source
  5. example (example at line 45) line 45 source
  6. example (example at line 49) line 49 source
  7. example (example at line 52) line 52 source
  8. example (example at line 55) line 55 source
  9. example (example at line 61) line 61 source
  10. example (example at line 70) line 70 source
  11. example (example at line 81) line 81 source
  12. example (example at line 84) line 84 source
  13. example (example at line 91) line 91 source
  14. example (example at line 95) line 95 source
  15. example (example at line 99) line 99 source
  16. example (example at line 107) line 107 source
  17. example (example at line 115) line 115 source
  18. example (example at line 121) line 121 source
  19. example (example at line 134) line 134 source
  20. example (example at line 138) line 138 source
  21. example (example at line 148) line 148 source
  22. example (example at line 156) line 156 source
  23. example (example at line 165) line 165 source
  24. example (example at line 177) line 177 source
  25. def inverse line 196 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/S02_Functions.lean:153 (same declaration text).

  26. theorem inverse_spec line 199 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/S02_Functions.lean:156 (same declaration text).

    Tactic trace: 19 steps

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

  27. example (example at line 207) line 207 source
  28. example (example at line 216) line 216 source
  29. example (example at line 219) line 219 source
  30. example (example at line 228) line 228 source
  31. theorem Cantor Cantor: no function from α to its power set is surjective line 237 source

    L4DEL explanation

    Build the set of elements not in their own image; it cannot be anyone's image.

    1. intro f surjf assumes f : α → Set α is surjective, and the goal becomes a contradiction.
    2. let S := { i | i ∉ f i } defines the diagonal set, and rcases surjf S gives j with f j = S.
    3. h₁ shows j ∉ f j, by assuming j ∈ f j, rewriting with f j = S to get j ∉ f j, and contradiction.
    4. From h₁, j ∈ S holds by definition of S (h₂), while rewriting f j = S in h₁ gives j ∉ S (h₃).
    5. h₂ and h₃ contradict each other, which closes the goal.

    Sources and attribution: Pinned Lean source (dd6d752fedb1)

    no axioms what this means

    Statement uses: Set, Not, Function.Surjective

    Proof uses: setOf, Membership.mem, Eq, Exists, False, Eq.mp, congrArg, False.elim

    2 instances, coercions and auxiliary constants left out.

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

    surjective: a function f is surjective when every element of its target equals f x for some x.

    Tactic trace: 12 steps

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

    theorem Cantor : ∀ f : α → Set α, ¬Surjective f := by
…

    Mentions: f