Documentation

Lean 4 Proof

theorem impossible_trinity {T_home T_foreign T_capital T_trade : ℝ}
    (h_total : totalBilateralFriction T_home T_foreign T_capital T_trade = 0)
    (h_cap : 0 ≤ T_capital) (h_trade : 0 ≤ T_trade) :
    T_home = T_foreign := by
  simp only [totalBilateralFriction] at h_total
  have h1 : |T_home - T_foreign| = 0 := by linarith [abs_nonneg (T_home - T_foreign)]
  linarith [abs_eq_zero.mp h1]

Dependency Graph

Location

thesis/CESProofs/Applications/OpenEconomy.lean:95

Module Section

Open Economy Monetary Transmission

In the same file