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

bec_temperature_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)

  41theorem bec_temperature_positive (m n : ℝ) (hm : 0 < m) (hn : 0 < n) :
  42    0 < bec_temperature m n := by

proof body

Term-mode proof.

  43  unfold bec_temperature
  44  apply mul_pos
  45  · positivity
  46  · apply Real.rpow_pos_of_pos; positivity
  47
  48/-! ## λ-point from Van der Waals Interactions -/
  49
  50/-- λ-point: T_lambda ≈ T_BEC × (1 - c₁ aₛ n^(1/3)) -/

depends on (3)

Lean names referenced from this declaration's body.