Documentation

Lean 4 Proof

theorem timescale_hierarchy {r₁ r₂ : ℝ} (hr₁ : 0 < r₁) (h12 : r₁ < r₂) :
    1 / r₂ < 1 / r₁ := by
  have hr₂ : 0 < r₂ := lt_trans hr₁ h12
  exact one_div_lt_one_div_of_lt hr₁ h12

Dependency Graph

Location

thesis/CESProofs/Dynamics/Relaxation.lean:96

Module Section

Results 1-7: Relaxation on the CES Potential Landscape

In the same file