Documentation

Lean 4 Proof

theorem divergence_raises_bilateral_friction {T_h T_f : ℝ}
    (h : T_h ≠ T_f) :
    0 < monetaryDivergenceFriction T_h T_f := by
  simp only [monetaryDivergenceFriction]
  exact abs_pos.mpr (sub_ne_zero.mpr h)

Dependency Graph

Location

thesis/CESProofs/Applications/OpenEconomy.lean:61

Module Section

Open Economy Monetary Transmission

In the same file