theorem proved term proof

`loadRatio_pos`

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

formal statement (Lean)

  93theorem loadRatio_pos {area demand : ℝ} (hArea : 0 < area) (hDemand : 0 < demand) :
  94    0 < loadRatio area demand := by

Term-mode proof.

  95  unfold loadRatio
  96  exact div_pos hDemand (bandwidth_pos hArea)
  97

Lean names referenced from this declaration's body.

loadRatio in IndisputableMonolith.Unification.CriticalRecognitionLoading decl_use
bandwidth_pos in IndisputableMonolith.Unification.RecognitionBandwidth decl_use