theorem proved term proof

`cmb_temperature_positive`

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

formal statement (Lean)

  71theorem cmb_temperature_positive (T_star z_star : ℝ)
  72    (hT : 0 < T_star) (hz : -1 < z_star) :
  73    0 < cmb_temperature T_star z_star := by

proof body

Term-mode proof.

  74  unfold cmb_temperature
  75  exact div_pos hT (by linarith)
  76
  77/-- **RS PREDICTION**: T₀ = 3000/(1101) ≈ 2.725 K. -/

depends on (3)

Lean names referenced from this declaration's body.

K in IndisputableMonolith.Constants decl_use
K in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
cmb_temperature in IndisputableMonolith.Physics.CMBTemperature decl_use