Documentation

Lean 4 Proof

theorem cleanShare_bounded {α ρ E_c E_d : ℝ}
    (hα : 0 < α) (hα1 : α < 1) (hEc : 0 < E_c) (hEd : 0 < E_d) :
    0 < cleanEnergyShare α ρ E_c E_d ∧ cleanEnergyShare α ρ E_c E_d < 1 :=
  ⟨capitalShare_pos (ρ := ρ) hα hα1 hEc hEd,
   capitalShare_lt_one hα hα1 hEc hEd⟩

Dependency Graph

Location

thesis/CESProofs/Macro/GreenTransition.lean:202

Module Section

Green Energy Transition Extension

In the same file