A filled nondegenerate triangle is exactly an intersection of three explicit halfspaces. In particular, endpoint and forbidden-point support conditions are proved for the actual convex-hull datatype, rather than a surrogate polygon.

def ConwaySoifer.cross (u v : Point) : ℝ

The coordinate determinant of two planar vectors.

Equations

• ConwaySoifer.cross u v = u.1 * v.2 - u.2 * v.1

def ConwaySoifer.linearForm (n : Point) : Point →ₗ[ℝ] ℝ

The real linear functional with the given coordinate coefficients.

Equations

• ConwaySoifer.linearForm n = { toFun := fun (p : ConwaySoifer.Point) => n.1 * p.1 + n.2 * p.2, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem ConwaySoifer.linearForm_apply (n p : Point) : (linearForm n) p = n.1 * p.1 + n.2 * p.2

@[simp]

theorem ConwaySoifer.cross_self (p : Point) : cross p p = 0

@[simp]

theorem ConwaySoifer.cross_zero_left (p : Point) : cross (0, 0) p = 0

@[simp]

theorem ConwaySoifer.cross_zero_right (p : Point) : cross p (0, 0) = 0

def ConwaySoifer.triangleDet (a b c : Point) : ℝ

The oriented doubled coordinate area of three vertices.

Equations

• ConwaySoifer.triangleDet a b c = ConwaySoifer.cross (b - a) (c - a)

noncomputable def ConwaySoifer.baryFirst (a b c p : Point) : ℝ

The barycentric coefficient of the second vertex relative to the first.

Equations

• ConwaySoifer.baryFirst a b c p = ConwaySoifer.cross (p - a) (c - a) / ConwaySoifer.triangleDet a b c

noncomputable def ConwaySoifer.barySecond (a b c p : Point) : ℝ

The barycentric coefficient of the third vertex relative to the first.

Equations

• ConwaySoifer.barySecond a b c p = ConwaySoifer.cross (b - a) (p - a) / ConwaySoifer.triangleDet a b c

noncomputable def ConwaySoifer.triangleNormals (a b c : Point) : Fin 3 → Point

The three outward normals, with orientation corrected by the determinant.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ConwaySoifer.triangleHalfspaces (a b c : Point) : HalfspaceSystem (Fin 3)

The three closed halfspaces determined by an oriented triangle.

Equations

• One or more equations did not get rendered due to their size.

theorem ConwaySoifer.HalfspaceSystem.convex_carrier {ι : Type u_1} (H : HalfspaceSystem ι) : Convex ℝ H.carrier

theorem ConwaySoifer.triangleHalfspaces_iff (a b c p : Point) : p ∈ (triangleHalfspaces a b c).carrier ↔ 0 ≤ baryFirst a b c p ∧ 0 ≤ barySecond a b c p ∧ baryFirst a b c p + barySecond a b c p ≤ 1

@[simp]

theorem ConwaySoifer.baryFirst_self (a b c : Point) : baryFirst a b c a = 0

@[simp]

theorem ConwaySoifer.barySecond_self (a b c : Point) : barySecond a b c a = 0

@[simp]

theorem ConwaySoifer.baryFirst_second (a b c : Point) (h : triangleDet a b c ≠ 0) : baryFirst a b c b = 1

@[simp]

theorem ConwaySoifer.barySecond_second (a b c : Point) : barySecond a b c b = 0

@[simp]

theorem ConwaySoifer.baryFirst_third (a b c : Point) : baryFirst a b c c = 0

@[simp]

theorem ConwaySoifer.barySecond_third (a b c : Point) (h : triangleDet a b c ≠ 0) : barySecond a b c c = 1

theorem ConwaySoifer.bary_expansion (a b c p : Point) (h : triangleDet a b c ≠ 0) : p = (1 - baryFirst a b c p - barySecond a b c p) • a + baryFirst a b c p • b + barySecond a b c p • c

theorem ConwaySoifer.convex_three_mem {S : Set Point} (hS : Convex ℝ S) {a b c : Point} (ha : a ∈ S) (hb : b ∈ S) (hc : c ∈ S) {u v : ℝ} (hu : 0 ≤ u) (hv : 0 ≤ v) (huv : u + v ≤ 1) : (1 - u - v) • a + u • b + v • c ∈ S

theorem ConwaySoifer.triangleHalfspaces_eq_convexHull (a b c : Point) (h : triangleDet a b c ≠ 0) : (triangleHalfspaces a b c).carrier = (convexHull ℝ) (Set.range ![a, b, c])

No equilateral assumption is needed for the geometric representation.

theorem ConwaySoifer.triangleDet_sq_identity (a b c : Point) : 3 * triangleDet a b c ^ 2 = 4 * sqDist b a * sqDist c a - (sqDist b a + sqDist c a - sqDist b c) ^ 2

theorem ConwaySoifer.EquilateralTriangle.det_sq (T : EquilateralTriangle) : triangleDet (T.vertices 0) (T.vertices 1) (T.vertices 2) ^ 2 = T.side ^ 4

theorem ConwaySoifer.EquilateralTriangle.det_ne_zero (T : EquilateralTriangle) (hs : 0 < T.side) : triangleDet (T.vertices 0) (T.vertices 1) (T.vertices 2) ≠ 0

noncomputable def ConwaySoifer.EquilateralTriangle.halfspaces (T : EquilateralTriangle) : HalfspaceSystem (Fin 3)

The halfspace system induced by the triangle's three vertices.

Equations

• T.halfspaces = ConwaySoifer.triangleHalfspaces (T.vertices 0) (T.vertices 1) (T.vertices 2)

theorem ConwaySoifer.EquilateralTriangle.carrier_eq_halfspaces (T : EquilateralTriangle) (hs : 0 < T.side) : T.carrier = T.halfspaces.carrier

theorem ConwaySoifer.EquilateralTriangle.full_endpoint_support (T : EquilateralTriangle) (hs : 0 < T.side) {v d : Point} (hv : v ∈ T.carrier) (hd : sqDist d (0, 0) = 1) : ∃ (i : Fin 3), 0 < (T.halfspaces.normal i) d ∧ (T.halfspaces.normal i) (linePoint v d (rayLen T v d)) = T.halfspaces.offset i ∧ ∀ q ∈ T.carrier, (T.halfspaces.normal i) q ≤ (T.halfspaces.normal i) (linePoint v d (rayLen T v d))

theorem ConwaySoifer.EquilateralTriangle.forbidden_support (T : EquilateralTriangle) (hs : 0 < T.side) {v d : Point} (hv : v ∈ T.carrier) {t : ℝ} (ht : 0 < t) (hout : linePoint v d t ∉ T.carrier) : ∃ (i : Fin 3), 0 < (T.halfspaces.normal i) d ∧ ∀ q ∈ T.carrier, (T.halfspaces.normal i) q < (T.halfspaces.normal i) (linePoint v d t)