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

temp_increases_with_mass

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)

  60theorem temp_increases_with_mass (M₁ M₂ R : ℝ)
  61    (hM₁ : 0 < M₁) (hM₂ : 0 < M₂) (hR : 0 < R) (h : M₁ < M₂) :
  62    virial_temperature M₁ R < virial_temperature M₂ R := by

proof body

Term-mode proof.

  63  unfold virial_temperature
  64  exact div_lt_div_of_pos_right h hR
  65
  66/-- **MAIN SEQUENCE RADIUS SCALING**: R ∝ M^0.8 (from homology relations).
  67    This scaling gives L ∝ M^3.9 when combined with luminosity transport. -/

depends on (6)

Lean names referenced from this declaration's body.