lemma proved term proof

`inner_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)

  50lemma inner_pos : 0 < hbar_codata * G_codata / (Real.pi * c_codata ^ 3) := by

proof body

Term-mode proof.

  51  apply div_pos (mul_pos hbar_codata_pos G_codata_pos)
  52  exact mul_pos Real.pi_pos (pow_pos c_codata_pos 3)
  53

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

inner_nonneg in IndisputableMonolith.Constants.Derivation decl_use
TurbineGeometry in IndisputableMonolith.Flight.TeslaTurbine decl_use

depends on (6)

Lean names referenced from this declaration's body.

c_codata in IndisputableMonolith.Constants.Derivation decl_use
c_codata_pos in IndisputableMonolith.Constants.Derivation decl_use
G_codata in IndisputableMonolith.Constants.Derivation decl_use
G_codata_pos in IndisputableMonolith.Constants.Derivation decl_use
hbar_codata in IndisputableMonolith.Constants.Derivation decl_use
hbar_codata_pos in IndisputableMonolith.Constants.Derivation decl_use