Simplex4D

formal source

  43
  44/-- A 4-simplex has 5 vertices and C(5,2) = 10 edges.
  45    The geometry is entirely determined by the 10 edge lengths. -/
  46structure Simplex4D where
  47  edges : Fin 10 → ℝ
  48  all_pos : ∀ i, 0 < edges i
  49
  50/-- A triangle (2-simplex) with 3 edge lengths. -/
  51structure Triangle where
  52  a : ℝ
  53  b : ℝ
  54  c : ℝ
  55  a_pos : 0 < a
  56  b_pos : 0 < b
  57  c_pos : 0 < c
  58
  59/-- Heron's formula for the area of a triangle. -/
  60noncomputable def Triangle.area (t : Triangle) : ℝ :=
  61  let s := (t.a + t.b + t.c) / 2
  62  Real.sqrt (s * (s - t.a) * (s - t.b) * (s - t.c))
  63
  64/-- Triangle area is non-negative (from Heron's formula with sqrt). -/
  65theorem Triangle.area_nonneg (t : Triangle) : 0 ≤ t.area := Real.sqrt_nonneg _
  66
  67/-- A tetrahedron (3-simplex) with 6 edge lengths.
  68    Vertices labeled 0,1,2,3; edge (i,j) has length l_ij. -/
  69structure Tetrahedron where
  70  l01 : ℝ
  71  l02 : ℝ
  72  l03 : ℝ
  73  l12 : ℝ
  74  l13 : ℝ
  75  l23 : ℝ
  76  l01_pos : 0 < l01