Documentation

Lean 4 Proof

theorem monotone_integration {T₁ T₂ Tstar₁ Tstar₂ : ℝ}
    (_hTs1 : 0 < Tstar₁) (_hTs2 : 0 < Tstar₂)
    (hT : T₁ ≤ T₂) (hTs : Tstar₂ ≤ Tstar₁) :
    -- If activity 1 is outsourced (T₁ ≥ T*₁), then activity 2 is also outsourced
    Tstar₁ ≤ T₁ → Tstar₂ ≤ T₂ := by
  intro h
  linarith

Dependency Graph

Location

thesis/CESProofs/Potential/FirmScope.lean:125

Module Section

Propositions 12-17 and Corollary 5:

In the same file