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

loadPenalty_zero_of_critical

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)

 199theorem loadPenalty_zero_of_critical
 200    {rhoMin area demand : ℝ}
 201    (h : InCriticalBand rhoMin area demand) :
 202    loadPenalty rhoMin area demand = 0 := by

proof body

Tactic-mode proof.

 203  unfold loadPenalty
 204  have hLeft : rhoMin - loadRatio area demand ≤ 0 := by
 205    linarith [h.1]
 206  have hRight : loadRatio area demand - 1 ≤ 0 := by
 207    linarith [h.2]
 208  rw [max_eq_left hLeft, max_eq_left hRight]
 209  ring
 210

used by (1)

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

depends on (3)

Lean names referenced from this declaration's body.