MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.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, 16 contain sorry, 0 declared as axioms

Imports (2)
Imported by 1 file
  1. theorem C03S01.my_lemma Exercise: a universally quantified statement (sorry) sorry line 10 source

    L4DEL explanation

    A statement of the form for-all-x-y-epsilon-then-implications is a function that takes numbers and proofs.

    1. This declaration is a stub: its body is sorry, so nothing is proved here.
    2. The statement says that for all real x, y, epsilon, if 0 < epsilon, epsilon <= 1, |x| < epsilon and |y| < epsilon then |x * y| < epsilon.
    3. The text after it applies my_lemma to a, b, delta and then to hypotheses h0, h1, ha, hb with #check, to show that instantiating a quantifier and discharging an implication are both just function application.

    See also: C03S01.my_lemma4@MIL/C03_Logic/solutions/Solutions_S01_Implication_and_the_Universal_Quantifier.lean

    Sources and attribution: Pinned Lean source (dd6d752fedb1)

    depends on sorry what this means

    Statement uses: Real, LT.lt, OfNat.ofNat, LE.le, abs, HMul.hMul

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat

    21 instances, coercions and auxiliary constants left out.

    theorem my_lemma : ∀ x y ε : ℝ, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε :=
…
  2. theorem C03S01.my_lemma2 sorry line 24 source

    depends on sorry what this means

    Statement uses: Real, LT.lt, OfNat.ofNat, LE.le, abs, HMul.hMul

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat

    21 instances, coercions and auxiliary constants left out.

  3. theorem C03S01.my_lemma3 sorry line 36 source

    depends on sorry what this means

    Statement uses: Real, LT.lt, OfNat.ofNat, LE.le, abs, HMul.hMul

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat

    21 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  4. theorem C03S01.my_lemma4 sorry line 41 source

    depends on sorry what this means

    Statement uses: Real, LT.lt, OfNat.ofNat, LE.le, abs, HMul.hMul

    Proof uses: Trans.trans, Eq, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat

    26 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C03_Logic/solutions/Solutions_S01_Implication_and_the_Universal_Quantifier.lean:6 (same statement text; different proof or body). Qualify references as C03S01.my_lemma4@path.

    Tactic trace: 2 steps

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

  5. def C03S01.FnUb line 50 source

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

    Statement uses: Real

    Proof uses: LE.le

    1 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C03_Logic/solutions/Solutions_S01_Implication_and_the_Universal_Quantifier.lean:15 (same declaration text).

  6. def C03S01.FnLb line 53 source

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

    Statement uses: Real

    Proof uses: LE.le

    1 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C03_Logic/solutions/Solutions_S01_Implication_and_the_Universal_Quantifier.lean:18 (same declaration text).

    Tactic trace: 5 steps

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

  7. example C03S01.(example at line 59) line 59 source
  8. example C03S01.(example at line 66) sorry line 66 source
  9. example C03S01.(example at line 69) sorry line 69 source
  10. example C03S01.(example at line 72) sorry line 72 source
  11. def C03S01.FnUb' line 83 source

    no axioms what this means

    Statement uses: PartialOrder

    Proof uses: LE.le

    2 instances, coercions and auxiliary constants left out.

  12. theorem C03S01.fnUb_add line 86 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: AddCommMonoid, PartialOrder, IsOrderedCancelAddMonoid, C03S01.FnUb', HAdd.hAdd

    Proof uses: add_le_add, LE.le

    13 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  13. example C03S01.(example at line 91) line 91 source
  14. example C03S01.(example at line 97) line 97 source
  15. example C03S01.(example at line 103) line 103 source
  16. example C03S01.(example at line 106) sorry line 106 source
  17. example C03S01.(example at line 109) sorry line 109 source
  18. def C03S01.FnEven line 112 source

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

    Statement uses: Real

    Proof uses: Eq, Neg.neg

    1 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C03_Logic/solutions/Solutions_S01_Implication_and_the_Universal_Quantifier.lean:67 (same declaration text).

  19. def C03S01.FnOdd line 115 source

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

    Statement uses: Real

    Proof uses: Eq, Neg.neg

    1 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C03_Logic/solutions/Solutions_S01_Implication_and_the_Universal_Quantifier.lean:70 (same declaration text).

    Tactic trace: 8 steps

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

  20. example C03S01.(example at line 118) line 118 source
  21. example C03S01.(example at line 125) sorry line 125 source
  22. example C03S01.(example at line 128) sorry line 128 source
  23. example C03S01.(example at line 131) sorry line 131 source
  24. example C03S01.(example at line 140) line 140 source
  25. theorem C03S01.Subset.refl line 144 source

    no axioms what this means

    Statement uses: Set, HasSubset.Subset

    Proof uses: Membership.mem

    2 instances, coercions and auxiliary constants left out.

  26. theorem C03S01.Subset.trans sorry line 146 source

    depends on sorry what this means

    Statement uses: Set, HasSubset.Subset

    Proof uses: 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/C03_Logic/solutions/Solutions_S01_Implication_and_the_Universal_Quantifier.lean:102 (same statement text; different proof or body). Qualify references as C03S01.Subset.trans@path.

    Tactic trace: 1 steps

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

  27. def C03S01.SetUb line 155 source

    no axioms what this means

    Statement uses: PartialOrder, Set

    Proof uses: Membership.mem, LE.le

    3 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C03_Logic/solutions/Solutions_S01_Implication_and_the_Universal_Quantifier.lean:111 (same declaration text).

    Tactic trace: 4 steps

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

  28. example C03S01.(example at line 158) sorry line 158 source
  29. example C03S01.(example at line 167) line 167 source
  30. example C03S01.(example at line 171) sorry line 171 source
  31. example C03S01.(example at line 177) sorry line 177 source