structure
definition
Triangle
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
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