Documentation

Lean 4 Proof

theorem crossing_irreversible {ρ_at_cross ρ_later : ℝ}
    (h_cross : 1 ≤ ρ_at_cross) (h_mono : ρ_at_cross ≤ ρ_later) :
    1 ≤ ρ_later :=
  le_trans h_cross h_mono

Dependency Graph

Location

thesis/CESProofs/Hierarchy/EndogenousCrossing.lean:195

Module Section

Proposition: Endogenous Crossing

In the same file