Documentation

Lean 4 Proof

theorem collapse_when_underfunded {R J c_min : ℝ}
    (hJ : 0 < J) (hR : R ≤ c_min * J) :
    producerProfit R J c_min ≤ 0 := by
  unfold producerProfit; rw [sub_nonpos, div_le_iff₀ hJ]; linarith

Dependency Graph

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:176

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file