MIL/C03_Logic/solutions/Solutions_S03_Negation.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def C03S03.FnUb line 9 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/S03_Negation.lean:14 (same declaration text).

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

3. def C03S03.FnHasUb line 15 source

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

   Statement uses: Real

   Proof uses: Exists, C03S03.FnUb

   Also declared: MIL/C03_Logic/S03_Negation.lean:20 (same declaration text).

4. def C03S03.FnHasLb line 18 source

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

   Statement uses: Real

   Proof uses: Exists, C03S03.FnLb

   Also declared: MIL/C03_Logic/S03_Negation.lean:23 (same declaration text).

   Tactic trace: 51 steps

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

5. example C03S03.(example at line 23) line 23 source
6. example C03S03.(example at line 29) line 29 source
7. example C03S03.(example at line 34) line 34 source
8. example C03S03.(example at line 40) line 40 source
9. example C03S03.(example at line 46) line 46 source
10. example C03S03.(example at line 56) line 56 source
11. example C03S03.(example at line 66) line 66 source
12. example C03S03.(example at line 71) line 71 source
13. example C03S03.(example at line 75) line 75 source
14. example C03S03.(example at line 81) line 81 source
15. example C03S03.(example at line 85) line 85 source
16. example C03S03.(example at line 94) line 94 source
17. example C03S03.(example at line 105) line 105 source