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

sound_speed_positive

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)

  44theorem sound_speed_positive (R : ℝ) (hR : -1 < R) :
  45    0 < sound_speed R := by

proof body

Term-mode proof.

  46  unfold sound_speed
  47  apply div_pos one_pos
  48  apply Real.sqrt_pos_of_pos
  49  linarith
  50
  51/-- In the limit R → 0 (radiation dominated): c_s → c/√3. -/

depends on (1)

Lean names referenced from this declaration's body.