lemma proved term proof

`lambda_PBM_pos`

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

formal statement (Lean)

 144lemma lambda_PBM_pos : 0 < lambda_PBM := by

proof body

Term-mode proof.

 145  unfold lambda_PBM
 146  exact div_pos (mul_pos planck_h_pos speed_of_light_pos) E_PBM_pos
 147
 148/-- λ_PBM falls in the therapeutic photobiomodulation window (750–780 nm). -/

used by (1)

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

rs_device in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use

depends on (4)

Lean names referenced from this declaration's body.

E_PBM_pos in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use
lambda_PBM in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use
planck_h_pos in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use
speed_of_light_pos in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use