MIL/C03_Logic/S05_Disjunction.lean

GitHub source file

23 declarations, 11 contain sorry, 0 declared as axioms

Imports (2)
Imported by 1 file
  1. example C03S05.(example at line 10) line 10 source
  2. example C03S05.(example at line 14) line 14 source
  3. example C03S05.(example at line 18) line 18 source
  4. example C03S05.(example at line 21) line 21 source
  5. example C03S05.(example at line 24) line 24 source
  6. example C03S05.(example at line 31) line 31 source
  7. example C03S05.(example at line 40) line 40 source
  8. example C03S05.(example at line 49) line 49 source
  9. theorem C03S05.MyAbs.le_abs_self sorry line 60 source

    depends on sorry what this means

    Statement uses: Real, LE.le, abs

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

    7 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C03_Logic/solutions/Solutions_S05_Disjunction.lean:12 (same statement text; different proof or body). Qualify references as C03S05.MyAbs.le_abs_self@path.

    Tactic trace: 1 steps

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

  10. theorem C03S05.MyAbs.neg_le_abs sorry line 63 source

    depends on sorry what this means

    Statement uses: Real, LE.le, Neg.neg, abs

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

    9 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C03_Logic/solutions/Solutions_S05_Disjunction.lean:18 (same statement text; different proof or body). Qualify references as C03S05.MyAbs.neg_le_abs@path.

    Tactic trace: 1 steps

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

  11. theorem C03S05.MyAbs.abs_add_le sorry line 66 source

    depends on sorry what this means

    Statement uses: Real, LE.le, abs, HAdd.hAdd

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

    11 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C03_Logic/solutions/Solutions_S05_Disjunction.lean:24 (same statement text; different proof or body). Qualify references as C03S05.MyAbs.abs_add_le@path.

    Tactic trace: 1 steps

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

  12. theorem C03S05.MyAbs.lt_abs sorry line 69 source

    depends on sorry what this means

    Statement uses: Real, Iff, LT.lt, abs, Or, Neg.neg

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

    9 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C03_Logic/solutions/Solutions_S05_Disjunction.lean:31 (same statement text; different proof or body). Qualify references as C03S05.MyAbs.lt_abs@path.

    Tactic trace: 1 steps

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

  13. theorem C03S05.MyAbs.abs_lt sorry line 72 source

    depends on sorry what this means

    Statement uses: Real, Iff, LT.lt, abs, And, Neg.neg

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

    9 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C03_Logic/solutions/Solutions_S05_Disjunction.lean:52 (same statement text; different proof or body). Qualify references as C03S05.MyAbs.abs_lt@path.

    Tactic trace: 34 steps

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

  14. example C03S05.(example at line 79) line 79 source
  15. example C03S05.(example at line 86) line 86 source
  16. example C03S05.(example at line 93) sorry line 93 source
  17. example C03S05.(example at line 96) sorry line 96 source
  18. example C03S05.(example at line 99) sorry line 99 source
  19. example C03S05.(example at line 106) sorry line 106 source
  20. example C03S05.(example at line 109) sorry line 109 source
  21. example C03S05.(example at line 114) line 114 source
  22. example C03S05.(example at line 120) line 120 source
  23. example C03S05.(example at line 126) sorry line 126 source