Documentation

Lean 4 Proof

theorem endogenous_crossing_summary
    (Q_star : ℝ) (hQ : 0 < Q_star)
    (I_nash I_coop : ℝ) (hI_coop : 0 < I_coop)
    (h_over : I_coop < I_nash) :
    -- Nash crossing time < cooperative crossing time
    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:270

Module Section

Proposition: Endogenous Crossing

In the same file