Documentation

Lean 4 Proof

theorem cleanEnergyCost_pos {p₀ β Q : ℝ}
    (hp₀ : 0 < p₀) (hQ : 0 < Q) :
    0 < cleanEnergyCost p₀ β Q :=
  wright_law_pos hp₀ hQ

Dependency Graph

Location

thesis/CESProofs/Macro/GreenTransition.lean:99

Module Section

Green Energy Transition Extension

In the same file