theorem proved term proof

`coolingFraction_pos`

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

formal statement (Lean)

  33theorem coolingFraction_pos : 0 < coolingFraction := by

Term-mode proof.

  34  unfold coolingFraction
  35  have := phi_gt_onePointFive; linarith
  36

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

cumulativeCooling_pos in IndisputableMonolith.Engineering.IdentityTickRefrigeratorSpec decl_use
cumulativeCooling_strict_mono in IndisputableMonolith.Engineering.IdentityTickRefrigeratorSpec decl_use
identityTickRefrigeratorCert in IndisputableMonolith.Engineering.IdentityTickRefrigeratorSpec decl_use
refrigerator_one_statement in IndisputableMonolith.Engineering.IdentityTickRefrigeratorSpec decl_use

Lean names referenced from this declaration's body.

phi_gt_onePointFive in IndisputableMonolith.Constants decl_use
coolingFraction in IndisputableMonolith.Engineering.IdentityTickRefrigeratorSpec decl_use