Documentation

Lean 4 Proof

theorem timescaleGap_monotone_in_relaxRate
    {r1 r2 : ℝ} (hr1 : 0 < r1) (hle : r1 ≤ r2)
    {v : ℝ} (hv : 0 < v) :
    v / r2 ≤ v / r1 :=
  div_le_div_of_nonneg_left (le_of_lt hv) hr1 hle

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/TwoWorldDefs.lean:198

Module Section

Two-World Economy: Price vs. Production Timescale Separation

In the same file