Documentation

Lean 4 Proof

theorem budget_monotone {B₁ B₂ p : ℝ}
    (hp : 0 < p) (hB : B₁ < B₂) :
    purchaseValue B₁ p < purchaseValue B₂ p := by
  unfold purchaseValue; exact div_lt_div_of_pos_right hB hp

Dependency Graph

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:342

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file