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) : ℝ :=
proof body
Definition body.
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. -/
used by (10)
From the project-wide theorem graph. These declarations reference this one in their body.