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

maintenanceDemand_nonneg

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)

 127theorem maintenanceDemand_nonneg {L : ℝ} (hL : 0 < L) :
 128    0 ≤ maintenanceDemand L := by

proof body

Term-mode proof.

 129  unfold maintenanceDemand
 130  exact mul_nonneg (le_of_lt barrierPeriod_pos) (Cost.Jcost_nonneg hL)
 131
 132/-- Maintenance demand is zero only when L = 1 (identity scale). -/

used by (1)

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

depends on (17)

Lean names referenced from this declaration's body.