MIL/C07_Structures/solutions/Solutions_S01_Structures.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. structure C06S01.Point line 9 source

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

   Distinct definitions of this name: MIL/C07_Structures/S01_Structures.lean:9 (same statement text; different proof or body). Qualify references as C06S01.Point@path.

2. def C06S01.Point.add line 16 source

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

   Statement uses: C06S01.Point

   Proof uses: C06S01.Point.mk, HAdd.hAdd, Real, C06S01.Point.x, C06S01.Point.y, C06S01.Point.z

   2 instances, coercions and auxiliary constants left out.

   Also declared: MIL/C07_Structures/S01_Structures.lean:43 (same declaration text).

3. theorem C06S01.Point.add_assoc line 19 source

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

   Statement uses: C06S01.Point, Eq, C06S01.Point.add

   Proof uses: of_eq_true, C06S01.Point.mk, HAdd.hAdd, Real, C06S01.Point.x, C06S01.Point.y, C06S01.Point.z, Eq.trans, True, congrFun', congrArg, congr, add_assoc, eq_self

   4 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: MIL/C07_Structures/S01_Structures.lean:86 (same statement text; different proof or body). Qualify references as C06S01.Point.add_assoc@path.

   Tactic trace: 1 steps

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

4. def C06S01.Point.smul line 22 source

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

   Statement uses: Real, C06S01.Point

   Proof uses: C06S01.Point.mk, HMul.hMul, C06S01.Point.x, C06S01.Point.y, C06S01.Point.z

   2 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: MIL/C07_Structures/S01_Structures.lean:89 (same statement text; different proof or body). Qualify references as C06S01.Point.smul@path.

5. theorem C06S01.Point.smul_distrib line 25 source

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

   Statement uses: Real, C06S01.Point, Eq, C06S01.Point.add, C06S01.Point.smul

   Proof uses: of_eq_true, C06S01.Point.mk, HAdd.hAdd, HMul.hMul, C06S01.Point.x, C06S01.Point.y, C06S01.Point.z, Eq.trans, True, congrArg, congr, mul_add, eq_self

   7 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: MIL/C07_Structures/S01_Structures.lean:92 (same statement text; different proof or body). Qualify references as C06S01.Point.smul_distrib@path.

   Tactic trace: 1 steps

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

6. structure C06S01.StandardTwoSimplex line 31 source

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

   Also declared: MIL/C07_Structures/S01_Structures.lean:98 (same declaration text).

7. def C06S01.StandardTwoSimplex.weightedAverage line 44 source

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

   Statement uses: Real, LE.le, OfNat.ofNat, C06S01.StandardTwoSimplex

   Proof uses: C06S01.StandardTwoSimplex.mk, HAdd.hAdd, HMul.hMul, C06S01.StandardTwoSimplex.x, HSub.hSub, C06S01.StandardTwoSimplex.y, C06S01.StandardTwoSimplex.z

   20 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: MIL/C07_Structures/S01_Structures.lean:131 (same statement text; different proof or body). Qualify references as C06S01.StandardTwoSimplex.weightedAverage@path.

   Tactic trace: 7 steps

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

8. structure C06S01.StandardSimplex line 64 source

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

   Statement uses: Nat

   Also declared: MIL/C07_Structures/S01_Structures.lean:141 (same declaration text).

9. def C06S01.StandardSimplex.midpoint line 71 source

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

   Statement uses: Nat, C06S01.StandardSimplex

   Proof uses: C06S01.StandardSimplex.mk, Fin, HDiv.hDiv, Real, HAdd.hAdd, C06S01.StandardSimplex.V, OfNat.ofNat

   10 instances, coercions and auxiliary constants left out.

   Also declared: MIL/C07_Structures/S01_Structures.lean:148 (same declaration text).

   Tactic trace: 7 steps

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

10. def C06S01.StandardSimplex.weightedAverage line 88 source

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

    Statement uses: Nat, Real, LE.le, OfNat.ofNat, C06S01.StandardSimplex

    Proof uses: C06S01.StandardSimplex.mk, Fin, HAdd.hAdd, HMul.hMul, C06S01.StandardSimplex.V, HSub.hSub

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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