theorem proved term proof

`cost_pos_off_equilibrium`

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

formal statement (Lean)

 142theorem cost_pos_off_equilibrium {x : ℝ} (hx : 0 < x) (hne : x ≠ 1) :
 143    0 < Cost.Jcost x :=

Term-mode proof.

 144  Cost.Jcost_pos_of_ne_one x hx hne
 145
 146/-! ## §6. Master certificate -/
 147

Lean names referenced from this declaration's body.