theorem proved term proof

`normalizedRatio_pos`

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

formal statement (Lean)

  52theorem normalizedRatio_pos (s : FiniteVolumeProfile) : 0 < normalizedRatio s := by

Term-mode proof.

  53  unfold normalizedRatio
  54  exact div_pos (lt_of_lt_of_le s.omegaRms_pos s.omegaRms_le_max) s.omegaRms_pos
  55

Lean names referenced from this declaration's body.