MIL/C07_Structures/S01_Structures.lean

GitHub source file

32 declarations, 4 contain sorry, 0 declared as axioms

Imports (3)
Imported by 1 file
  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/solutions/Solutions_S01_Structures.lean:9 (same statement text; different proof or body). Qualify references as C06S01.Point@path.

    Tactic trace: 3 steps

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

  2. example C06S01.(example at line 16) line 16 source
  3. def C06S01.myPoint1 line 20 source

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

    Statement uses: C06S01.Point

    Proof uses: C06S01.Point.mk, OfNat.ofNat, Real, Neg.neg

    7 instances, coercions and auxiliary constants left out.

  4. def C06S01.myPoint2 line 25 source

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

    Statement uses: C06S01.Point

    Proof uses: C06S01.Point.mk, OfNat.ofNat, Real, Neg.neg

    7 instances, coercions and auxiliary constants left out.

  5. def C06S01.myPoint3 line 28 source

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

    Statement uses: C06S01.Point

    Proof uses: C06S01.Point.mk, OfNat.ofNat, Real, Neg.neg

    7 instances, coercions and auxiliary constants left out.

  6. def C06S01.myPoint4 line 31 source

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

    Statement uses: C06S01.Point

    Proof uses: C06S01.Point.mk, OfNat.ofNat, Real, Neg.neg

    7 instances, coercions and auxiliary constants left out.

  7. structure C06S01.Point' line 34 source

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

  8. def C06S01.Point.add line 43 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/solutions/Solutions_S01_Structures.lean:16 (same declaration text).

  9. def C06S01.Point.add' line 46 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.

  10. theorem C06S01.Point.add_comm line 61 source

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

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

    Proof uses: Eq.mpr, C06S01.Point.mk, HAdd.hAdd, Real, C06S01.Point.x, C06S01.Point.y, C06S01.Point.z, id, congrArg, C06S01.Point.add.eq_1, C06S01.Point.ext, add_comm

    4 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  11. example C06S01.Point.(example at line 66) line 66 source
  12. theorem C06S01.Point.add_x line 68 source

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

    Statement uses: C06S01.Point, Eq, Real, C06S01.Point.x, C06S01.Point.add, HAdd.hAdd

    Proof uses: rfl

    2 instances, coercions and auxiliary constants left out.

  13. def C06S01.Point.addAlt line 71 source

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

    Statement uses: C06S01.Point

    Proof uses: C06S01.Point.addAlt.match_1, Real, C06S01.Point.mk, HAdd.hAdd

    2 instances, coercions and auxiliary constants left out.

  14. def C06S01.Point.addAlt' line 74 source

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

    Statement uses: C06S01.Point

    Proof uses: C06S01.Point.addAlt.match_1, Real, C06S01.Point.mk, HAdd.hAdd

    2 instances, coercions and auxiliary constants left out.

  15. theorem C06S01.Point.addAlt_x line 77 source

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

    Statement uses: C06S01.Point, Eq, Real, C06S01.Point.x, C06S01.Point.addAlt, HAdd.hAdd

    Proof uses: Eq.refl

    2 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  16. theorem C06S01.Point.addAlt_comm line 80 source

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

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

    Proof uses: Eq.mpr, C06S01.Point.mk, HAdd.hAdd, Real, C06S01.Point.x, C06S01.Point.y, C06S01.Point.z, id, congrArg, C06S01.Point.addAlt.eq_1, C06S01.Point.ext, add_comm

    4 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  17. theorem C06S01.Point.add_assoc sorry line 86 source

    depends on sorry what this means

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

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    1 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C07_Structures/solutions/Solutions_S01_Structures.lean:19 (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.

  18. def C06S01.Point.smul sorry line 89 source

    depends on sorry what this means

    Statement uses: Real, C06S01.Point

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    1 instances, coercions and auxiliary constants left out.

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

  19. theorem C06S01.Point.smul_distrib sorry line 92 source

    depends on sorry what this means

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

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    1 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C07_Structures/solutions/Solutions_S01_Structures.lean:25 (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.

  20. structure C06S01.StandardTwoSimplex line 98 source

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

    Also declared: MIL/C07_Structures/solutions/Solutions_S01_Structures.lean:31 (same declaration text).

  21. def C06S01.StandardTwoSimplex.swapXy line 109 source

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

    Statement uses: C06S01.StandardTwoSimplex

    Proof uses: C06S01.StandardTwoSimplex.mk, C06S01.StandardTwoSimplex.y, C06S01.StandardTwoSimplex.x, C06S01.StandardTwoSimplex.z, C06S01.StandardTwoSimplex.y_nonneg, C06S01.StandardTwoSimplex.x_nonneg, C06S01.StandardTwoSimplex.z_nonneg

    1 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  22. def C06S01.StandardTwoSimplex.midpoint line 121 source

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

    Statement uses: C06S01.StandardTwoSimplex

    Proof uses: C06S01.StandardTwoSimplex.mk, HDiv.hDiv, Real, HAdd.hAdd, C06S01.StandardTwoSimplex.x, OfNat.ofNat, C06S01.StandardTwoSimplex.y, C06S01.StandardTwoSimplex.z

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  23. def C06S01.StandardTwoSimplex.weightedAverage sorry line 131 source

    depends on sorry what this means

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

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

    11 instances, coercions and auxiliary constants left out.

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

  24. structure C06S01.StandardSimplex line 141 source

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

    Statement uses: Nat

    Also declared: MIL/C07_Structures/solutions/Solutions_S01_Structures.lean:64 (same declaration text).

  25. def C06S01.StandardSimplex.midpoint line 148 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/solutions/Solutions_S01_Structures.lean:71 (same declaration text).

    Tactic trace: 7 steps

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

  26. structure C06S01.IsLinear line 163 source

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

    Statement uses: Real

  27. def C06S01.Point'' line 175 source

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

    Proof uses: Prod, Real

  28. def C06S01.IsLinear' line 178 source

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

    Statement uses: Real

    Proof uses: And, Eq, HAdd.hAdd, HMul.hMul

    4 instances, coercions and auxiliary constants left out.

  29. def C06S01.PReal line 181 source

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

    Proof uses: Subtype, Real, LT.lt, OfNat.ofNat

    3 instances, coercions and auxiliary constants left out.

  30. def C06S01.StandardTwoSimplex' line 194 source

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

    Proof uses: Subtype, Prod, Real, And, LE.le, OfNat.ofNat, Prod.fst, Prod.snd, Eq, HAdd.hAdd

    7 instances, coercions and auxiliary constants left out.

  31. def C06S01.StandardSimplex' line 197 source

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

    Statement uses: Nat

    Proof uses: Subtype, Fin, Real, And, LE.le, OfNat.ofNat, Eq, Finset.sum, Finset.univ

    7 instances, coercions and auxiliary constants left out.

  32. def C06S01.StdSimplex line 200 source

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

    Proof uses: Sigma, Nat, C06S01.StandardSimplex