Documentation

Lean 4 Proof

theorem steadyStateKY_decreasing_in_δ {s δ₁ δ₂ : ℝ} (hs : 0 < s)
    (hδ₁ : 0 < δ₁) (_hδ₂ : 0 < δ₂) (hδ : δ₁ < δ₂) :
    steadyStateKY s δ₂ < steadyStateKY s δ₁ := by
  simp only [steadyStateKY]
  exact div_lt_div_of_pos_left hs hδ₁ hδ

Dependency Graph

Location

thesis/CESProofs/Macro/Accumulation.lean:106

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file