Documentation

Lean 4 Proof

theorem self_undermining {Q_star I₁ I₂ : ℝ}
    (hQ : 0 < Q_star) (hI₁ : 0 < I₁) (_hI₂ : 0 < I₂)
    (hI : I₁ < I₂) :
    Q_star / I₂ < Q_star / I₁ :=
  div_lt_div_of_pos_left hQ hI₁ hI

Dependency Graph

Location

thesis/CESProofs/Hierarchy/EndogenousCrossing.lean:187

Module Section

Proposition: Endogenous Crossing

In the same file