MIL/C03_Logic/S04_Conjunction_and_Iff.lean

GitHub source file

31 declarations, 8 contain sorry, 0 declared as axioms

Imports (3)
Imported by 1 file
  1. example C03S04.(example at line 7) line 7 source
  2. example C03S04.(example at line 14) line 14 source
  3. example C03S04.(example at line 17) line 17 source
  4. example C03S04.(example at line 23) line 23 source
  5. example C03S04.(example at line 28) line 28 source
  6. example C03S04.(example at line 32) line 32 source
  7. example C03S04.(example at line 35) line 35 source
  8. example C03S04.(example at line 40) line 40 source
  9. example C03S04.(example at line 46) line 46 source
  10. example C03S04.(example at line 52) line 52 source
  11. example C03S04.(example at line 58) line 58 source
  12. example C03S04.(example at line 63) line 63 source
  13. example C03S04.(example at line 66) sorry line 66 source
  14. example C03S04.(example at line 69) line 69 source
  15. example C03S04.(example at line 72) line 72 source
  16. example C03S04.(example at line 76) line 76 source
  17. example C03S04.(example at line 79) line 79 source
  18. example C03S04.(example at line 83) line 83 source
  19. example C03S04.(example at line 88) line 88 source
  20. example C03S04.(example at line 93) line 93 source
  21. example C03S04.(example at line 101) line 101 source
  22. example C03S04.(example at line 104) sorry line 104 source
  23. theorem C03S04.aux sorry line 107 source

    depends on sorry what this means

    Statement uses: Real, Eq, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat

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

    24 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C03_Logic/solutions/Solutions_S04_Conjunction_and_Iff.lean:30 (same statement text; different proof or body). Qualify references as C03S04.aux@path.

    Tactic trace: 8 steps

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

  24. example C03S04.(example at line 111) sorry line 111 source
  25. example C03S04.(example at line 116) line 116 source
  26. example C03S04.(example at line 121) line 121 source
  27. theorem C03S04.not_monotone_iff line 127 source

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

    Statement uses: Real, Iff, Not, Monotone, Exists, And, LE.le, GT.gt

    Proof uses: Eq.mpr, id, Eq, congrArg, Monotone.eq_1, LT.lt, congrFun', Eq.trans, Mathlib.Tactic.Push.not_forall_eq, funext, Iff.rfl

    13 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C03_Logic/solutions/Solutions_S04_Conjunction_and_Iff.lean:44 (same declaration text).

    Tactic trace: 10 steps

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

  28. example C03S04.(example at line 132) sorry line 132 source
  29. example C03S04.(example at line 139) sorry line 139 source
  30. example C03S04.(example at line 149) sorry line 149 source
  31. example C03S04.(example at line 153) sorry line 153 source