Documentation

Lean 4 Proof

private lemma continuous_min_div (S_crit : ℝ) :
    Continuous (fun S : ℝ => min 1 (S / S_crit)) :=
  continuous_const.min (continuous_id.div_const S_crit)

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:403

Module Section

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

In the same file