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

hbar_derived_pos

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)

 112lemma hbar_derived_pos (τ G_val c_val : ℝ) (hτ : 0 < τ) (hG : 0 < G_val) (hc : 0 < c_val) :
 113    0 < hbar_derived τ G_val c_val := by

proof body

Term-mode proof.

 114  unfold hbar_derived
 115  apply div_pos _ hG
 116  exact mul_pos (mul_pos Real.pi_pos (pow_pos hc 5)) (sq_pos_of_pos hτ)
 117
 118/-- **Theorem**: hbar_derived tau0 G_codata c_codata = hbar_codata -/

depends on (8)

Lean names referenced from this declaration's body.