MIL/C03_Logic/solutions/Solutions_S02_The_Existential_Quantifier.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
  1. def C03S02.FnUb line 8 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/S02_The_Existential_Quantifier.lean:28 (same declaration text).

  2. def C03S02.FnLb line 11 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/S02_The_Existential_Quantifier.lean:31 (same declaration text).

  3. def C03S02.FnHasUb line 14 source

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

    Statement uses: Real

    Proof uses: Exists, C03S02.FnUb

    Also declared: MIL/C03_Logic/S02_The_Existential_Quantifier.lean:34 (same declaration text).

  4. def C03S02.FnHasLb line 17 source

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

    Statement uses: Real

    Proof uses: Exists, C03S02.FnLb

    Also declared: MIL/C03_Logic/S02_The_Existential_Quantifier.lean:37 (same declaration text).

  5. theorem C03S02.fnUb_add line 20 source

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

    Statement uses: Real, C03S02.FnUb, HAdd.hAdd

    Proof uses: add_le_add, LE.le

    10 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C03_Logic/S02_The_Existential_Quantifier.lean:40 (same declaration text).

    Tactic trace: 28 steps

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

  6. example C03S02.(example at line 28) line 28 source
  7. example C03S02.(example at line 35) line 35 source
  8. example C03S02.(example at line 46) line 46 source
  9. example C03S02.(example at line 51) line 51 source
  10. example C03S02.(example at line 62) line 62 source
  11. example C03S02.(example at line 67) line 67 source
  12. example C03S02.(example at line 79) line 79 source