Documentation

Lean 4 Proof

theorem crossingProduction_pos {p₀ p_d τ β : ℝ}
    (hp₀ : 0 < p₀) (hpdτ : 0 < p_d + τ) :
    0 < crossingProduction p₀ p_d τ β :=
  rpow_pos_of_pos (div_pos hp₀ hpdτ) _

Dependency Graph

Location

thesis/CESProofs/Macro/GreenTransition.lean:136

Module Section

Green Energy Transition Extension

In the same file