structure definition def or abbrev

`Simplex4D`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  46structure Simplex4D where
  47  edges : Fin 10 → ℝ
  48  all_pos : ∀ i, 0 < edges i
  49
  50/-- A triangle (2-simplex) with 3 edge lengths. -/

Lean names referenced from this declaration's body.