Documentation

TauCeti.Analysis.Green.Polygonal.Geometry

Supporting halfplanes of a planar triangle #

The interior of a convex triangle lies strictly on the side of each edge containing the third vertex. The determinant records the orientation of the ordered triple.

source
def TauCeti.Green.triangleDet (c p q : ℂ) :
ℝ

The real determinant of the two edges based at the first vertex.

Equations
Instances For
    source
    theorem TauCeti.Green.triangleDet_def (c p q : ℂ) :
    triangleDet c p q = (p - c).re * (q - c).im - (p - c).im * (q - c).re

    The oriented determinant in real and imaginary coordinates.

    source
    theorem TauCeti.Green.im_div_sub_eq_triangleDet (p q z : ℂ) :
    ((z - p) / (q - p)).im = triangleDet p q z / Complex.normSq (q - p)

    The imaginary height relative to an edge is its oriented determinant divided by norm squared.

    source
    theorem TauCeti.Green.triangleDet_cyclic (c p q : ℂ) :
    triangleDet p q c = triangleDet c p q

    Cyclically relabelling vertices preserves the oriented determinant.

    source
    theorem TauCeti.Green.triangleDet_swap (c p q : ℂ) :
    triangleDet c q p = -triangleDet c p q

    Interchanging two vertices negates the oriented determinant.

    source
    theorem TauCeti.Green.sub_ne_zero_of_triangleDet_pos {p q r : ℂ} (h : 0 < triangleDet p q r) :
    q - p ≠ 0

    A positive determinant ensures that the first edge is nondegenerate.

    source
    theorem TauCeti.Green.im_div_sub_pos_of_triangleDet_pos {p q r : ℂ} (h : 0 < triangleDet p q r) :
    0 < ((r - p) / (q - p)).im

    A positive oriented determinant places the third vertex strictly left of the first edge.

    source
    theorem TauCeti.Green.im_div_pos_of_mem_interior_convexHull_triangle {p q r z : ℂ} (hpq : q - p ≠ 0) (hr : 0 ≤ ((r - p) / (q - p)).im) (hz : z ∈ interior ((convexHull ℝ) {p, q, r})) :
    0 < ((z - p) / (q - p)).im

    An interior point lies strictly on the side of an edge containing the third vertex.

    source
    theorem TauCeti.Green.interior_convexHull_triangle_eq_empty {c p q : ℂ} (hdet : triangleDet c p q = 0) :
    interior ((convexHull ℝ) {c, p, q}) = ∅

    A degenerate planar triangle has empty interior.

    source
    theorem TauCeti.Green.volume_convexHull_triangle_eq_zero {c p q : ℂ} (hdet : triangleDet c p q = 0) :
    MeasureTheory.volume ((convexHull ℝ) {c, p, q}) = 0

    A degenerate planar triangle has area zero.