Documentation

Lean 4 Proof

theorem wright_law_pos {c₀ α Q : ℝ}
    (hc₀ : 0 < c₀) (hQ : 0 < Q) :
    0 < c₀ * Q ^ (-α) :=
  mul_pos hc₀ (rpow_pos_of_pos hQ _)

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/EndogenousCrossing.lean:47

Module Section

Proposition: Endogenous Crossing

In the same file