Documentation

Lean 4 Proof

theorem nash_crosses_faster {Q_star I_nash I_coop : ℝ}
    (hQ : 0 < Q_star) (hI_coop : 0 < I_coop) (_hI_nash : 0 < I_nash)
    (h_over : I_coop < I_nash) :
    Q_star / I_nash < Q_star / I_coop :=
  div_lt_div_of_pos_left hQ hI_coop h_over

Dependency Graph

Location

thesis/CESProofs/Hierarchy/EndogenousCrossing.lean:226

Module Section

Proposition: Endogenous Crossing

In the same file