Documentation

Lean 4 Proof

theorem energyCESInner_pos {α ρ E_c E_d : ℝ}
    (hα : 0 < α) (hα1 : α < 1) (hEc : 0 < E_c) (hEd : 0 < E_d) :
    0 < energyCESInner α ρ E_c E_d :=
  cesInner_pos hα hα1 hEc hEd

Dependency Graph

Location

thesis/CESProofs/Macro/GreenTransition.lean:79

Module Section

Green Energy Transition Extension

In the same file