structure
definition
Triangle
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Gravity.ReggeCalculus on GitHub at line 51.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
77 l02_pos : 0 < l02
78 l03_pos : 0 < l03
79 l12_pos : 0 < l12
80 l13_pos : 0 < l13
81 l23_pos : 0 < l23