Documentation

Lean 4 Proof

theorem triffin_time_pos {S_max g_settle : ℝ}
    (hS : 0 < S_max) (hg : 0 < g_settle) :
    0 < triffinTime S_max g_settle :=
  div_pos hS hg

Dependency Graph

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:292

Module Section

Paper 7: Settlement Feedback and Monetary Policy in a Mesh Economy

In the same file