def definition def or abbrev

`payment`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 126def payment₀ (b₀ b₁ : ℝ) : ℝ :=

proof body

Definition body.

 127  if b₀ ≥ b₁ then b₁ else 0
 128
 129/-- The payment by agent `1` under bid pair `(b₀, b₁)`. Equals `b₀`
 130if 1 wins, else 0. -/
 131def payment₁ (b₀ b₁ : ℝ) : ℝ :=
 132  if b₀ ≥ b₁ then 0 else b₀
 133
 134/-- Agent 0's utility under valuation `v₀` and bid pair `(b₀, b₁)`. -/