Documentation

Lean 4 Proof

theorem friction_increases_with_cost {T₀ f_c₁ f_c₂ : ℝ}
    (hT₀ : 0 < T₀) (hf : f_c₁ < f_c₂) :
    T₀ * f_c₁ < T₀ * f_c₂ :=
  mul_lt_mul_of_pos_left hf hT₀

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/EndogenousCrossing.lean:56

Module Section

Proposition: Endogenous Crossing

In the same file