MIL/C03_Logic/S03_Negation.lean

GitHub source file

28 declarations, 14 contain sorry, 0 declared as axioms

Imports (2)
Imported by 1 file
  1. example C03S03.(example at line 9) line 9 source
  2. def C03S03.FnUb line 14 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_S03_Negation.lean:9 (same declaration text).

  3. def C03S03.FnLb line 17 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_S03_Negation.lean:12 (same declaration text).

  4. def C03S03.FnHasUb line 20 source

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

    Statement uses: Real

    Proof uses: Exists, C03S03.FnUb

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

  5. def C03S03.FnHasLb line 23 source

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

    Statement uses: Real

    Proof uses: Exists, C03S03.FnLb

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

    Tactic trace: 43 steps

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

  6. example C03S03.(example at line 28) line 28 source
  7. example C03S03.(example at line 35) sorry line 35 source
  8. example C03S03.(example at line 38) sorry line 38 source
  9. example C03S03.(example at line 46) sorry line 46 source
  10. example C03S03.(example at line 49) sorry line 49 source
  11. example C03S03.(example at line 52) sorry line 52 source
  12. example C03S03.(example at line 59) sorry line 59 source
  13. example C03S03.(example at line 67) sorry line 67 source
  14. example C03S03.(example at line 70) sorry line 70 source
  15. example C03S03.(example at line 73) sorry line 73 source
  16. example C03S03.(example at line 76) sorry line 76 source
  17. example C03S03.(example at line 79) line 79 source
  18. example C03S03.(example at line 87) sorry line 87 source
  19. example C03S03.(example at line 90) sorry line 90 source
  20. example C03S03.(example at line 98) sorry line 98 source
  21. example C03S03.(example at line 101) line 101 source
  22. example C03S03.(example at line 105) line 105 source
  23. example C03S03.(example at line 110) sorry line 110 source
  24. example C03S03.(example at line 113) line 113 source
  25. example C03S03.(example at line 117) line 117 source
  26. example C03S03.(example at line 127) line 127 source
  27. example C03S03.(example at line 131) line 131 source
  28. example C03S03.(example at line 134) line 134 source