theorem C06S01.Point.ext_iff {x : C06S01.Point} {y : C06S01.Point} : x = y ↔ x.x = y.x ∧ x.y = y.y ∧ x.z = y.z

theorem C06S01.Point.ext {x : C06S01.Point} {y : C06S01.Point} (x : x✝.x = y✝.x) (y : x✝.y = y✝.y) (z : x✝.z = y✝.z) : x✝ = y✝

structure C06S01.Point : Type

• x : ℝ
• y : ℝ
• z : ℝ

def C06S01.myPoint1 : C06S01.Point

Equations

• C06S01.myPoint1 = { x := 2, y := -1, z := 4 }

def C06S01.myPoint2 : C06S01.Point

Equations

• C06S01.myPoint2 = { x := 2, y := -1, z := 4 }

def C06S01.myPoint3 : C06S01.Point

Equations

• C06S01.myPoint3 = { x := 2, y := -1, z := 4 }

structure C06S01.Point' : Type

• build :: (
• x : ℝ
• y : ℝ
• z : ℝ
• )

def C06S01.Point.add (a : C06S01.Point) (b : C06S01.Point) : C06S01.Point

Equations

• a.add b = { x := a.x + b.x, y := a.y + b.y, z := a.z + b.z }

def C06S01.Point.add' (a : C06S01.Point) (b : C06S01.Point) : C06S01.Point

Equations

• a.add' b = { x := a.x + b.x, y := a.y + b.y, z := a.z + b.z }

theorem C06S01.Point.add_comm (a : C06S01.Point) (b : C06S01.Point) : a.add b = b.add a

theorem C06S01.Point.add_x (a : C06S01.Point) (b : C06S01.Point) : (a.add b).x = a.x + b.x

def C06S01.Point.addAlt : C06S01.Point → C06S01.Point → C06S01.Point

Equations

• { x := x₁, y := y₁, z := z₁ }.addAlt { x := x₂, y := y₂, z := z₂ } = { x := x₁ + x₂, y := y₁ + y₂, z := z₁ + z₂ }

def C06S01.Point.addAlt' : C06S01.Point → C06S01.Point → C06S01.Point

Equations

• { x := x₁, y := y₁, z := z₁ }.addAlt' { x := x₂, y := y₂, z := z₂ } = { x := x₁ + x₂, y := y₁ + y₂, z := z₁ + z₂ }

theorem C06S01.Point.addAlt_x (a : C06S01.Point) (b : C06S01.Point) : (a.addAlt b).x = a.x + b.x

theorem C06S01.Point.addAlt_comm (a : C06S01.Point) (b : C06S01.Point) : a.addAlt b = b.addAlt a

theorem C06S01.Point.add_assoc (a : C06S01.Point) (b : C06S01.Point) (c : C06S01.Point) : (a.add b).add c = a.add (b.add c)

def C06S01.Point.smul (r : ℝ) (a : C06S01.Point) : C06S01.Point

Equations

• C06S01.Point.smul r a = sorryAx C06S01.Point

theorem C06S01.Point.smul_distrib (r : ℝ) (a : C06S01.Point) (b : C06S01.Point) : (C06S01.Point.smul r a).add (C06S01.Point.smul r b) = C06S01.Point.smul r (a.add b)

structure C06S01.StandardTwoSimplex : Type

• x : ℝ
• y : ℝ
• z : ℝ
• x_nonneg : 0 ≤ self.x
• y_nonneg : 0 ≤ self.y
• z_nonneg : 0 ≤ self.z
• sum_eq : self.x + self.y + self.z = 1

theorem C06S01.StandardTwoSimplex.x_nonneg (self : C06S01.StandardTwoSimplex) : 0 ≤ self.x

theorem C06S01.StandardTwoSimplex.y_nonneg (self : C06S01.StandardTwoSimplex) : 0 ≤ self.y

theorem C06S01.StandardTwoSimplex.z_nonneg (self : C06S01.StandardTwoSimplex) : 0 ≤ self.z

theorem C06S01.StandardTwoSimplex.sum_eq (self : C06S01.StandardTwoSimplex) : self.x + self.y + self.z = 1

def C06S01.StandardTwoSimplex.swapXy (a : C06S01.StandardTwoSimplex) : C06S01.StandardTwoSimplex

Equations

• a.swapXy = { x := a.y, y := a.x, z := a.z, x_nonneg := ⋯, y_nonneg := ⋯, z_nonneg := ⋯, sum_eq := ⋯ }

def C06S01.StandardTwoSimplex.midpoint (a : C06S01.StandardTwoSimplex) (b : C06S01.StandardTwoSimplex) : C06S01.StandardTwoSimplex

Equations

• a.midpoint b = { x := (a.x + b.x) / 2, y := (a.y + b.y) / 2, z := (a.z + b.z) / 2, x_nonneg := ⋯, y_nonneg := ⋯, z_nonneg := ⋯, sum_eq := ⋯ }

def C06S01.StandardTwoSimplex.weightedAverage (lambda : ℝ) (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1) (a : C06S01.StandardTwoSimplex) (b : C06S01.StandardTwoSimplex) : C06S01.StandardTwoSimplex

Equations

• C06S01.StandardTwoSimplex.weightedAverage lambda lambda_nonneg lambda_le a b = sorryAx C06S01.StandardTwoSimplex

structure C06S01.StandardSimplex (n : ℕ) : Type

• V : Fin n → ℝ
• NonNeg : ∀ (i : Fin n), 0 ≤ self.V i
• sum_eq_one : ∑ i : Fin n, self.V i = 1

theorem C06S01.StandardSimplex.NonNeg {n : ℕ} (self : C06S01.StandardSimplex n) (i : Fin n) : 0 ≤ self.V i

theorem C06S01.StandardSimplex.sum_eq_one {n : ℕ} (self : C06S01.StandardSimplex n) : ∑ i : Fin n, self.V i = 1

def C06S01.StandardSimplex.midpoint (n : ℕ) (a : C06S01.StandardSimplex n) (b : C06S01.StandardSimplex n) : C06S01.StandardSimplex n

Equations

• C06S01.StandardSimplex.midpoint n a b = { V := fun (i : Fin n) => (a.V i + b.V i) / 2, NonNeg := ⋯, sum_eq_one := ⋯ }

structure C06S01.IsLinear (f : ℝ → ℝ) : Type

• is_additive : ∀ (x y : ℝ), f (x + y) = f x + f y
• preserves_mul : ∀ (x c : ℝ), f (c * x) = c * f x

theorem C06S01.IsLinear.is_additive {f : ℝ → ℝ} (self : C06S01.IsLinear f) (x : ℝ) (y : ℝ) : f (x + y) = f x + f y

theorem C06S01.IsLinear.preserves_mul {f : ℝ → ℝ} (self : C06S01.IsLinear f) (x : ℝ) (c : ℝ) : f (c * x) = c * f x

def C06S01.Point'' : Type

Equations

• C06S01.Point'' = (ℝ × ℝ × ℝ)

def C06S01.IsLinear' (f : ℝ → ℝ) : Prop

Equations

• C06S01.IsLinear' f = ((∀ (x y : ℝ), f (x + y) = f x + f y) ∧ ∀ (x c : ℝ), f (c * x) = c * f x)

def C06S01.PReal : Type

Equations

• C06S01.PReal = { y : ℝ // 0 < y }

def C06S01.StandardTwoSimplex' : Type

Equations

• C06S01.StandardTwoSimplex' = { p : ℝ × ℝ × ℝ // 0 ≤ p.1 ∧ 0 ≤ p.2.1 ∧ 0 ≤ p.2.2 ∧ p.1 + p.2.1 + p.2.2 = 1 }

def C06S01.StandardSimplex' (n : ℕ) : Type

Equations

• C06S01.StandardSimplex' n = { v : Fin n → ℝ // (∀ (i : Fin n), 0 ≤ v i) ∧ ∑ i : Fin n, v i = 1 }

def C06S01.StdSimplex : Type

Equations

• C06S01.StdSimplex = ((n : ℕ) × C06S01.StandardSimplex n)