pith. machine review for the scientific record. sign in
theorem proved term proof

cubicArea_singleton

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 138theorem cubicArea_singleton {n : ℕ} (L : EdgeLengthField n)
 139    (i j : Fin n) (w : ℝ) (hw : 0 ≤ w) :
 140    cubicArea L (singletonHinge i j w hw)
 141    = jcost_to_regge_factor * w / 2 := by

proof body

Term-mode proof.

 142  show (match (singletonHinge i j w hw).edges with
 143        | [(i', j')] =>
 144            jcost_to_regge_factor * (singletonHinge i j w hw).weight (i', j') / 2
 145        | _ => 0) = _
 146  rw [singletonHinge_edges]
 147  simp only
 148  rw [singletonHinge_weight]
 149
 150/-- `cubicArea` is nonnegative. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (12)

Lean names referenced from this declaration's body.