Documentation

Lean 4 Proof

theorem below_healthy_attracts {R J c_min : ℝ}
    (hc : 0 < c_min) (hJ : 0 < J)
    (hbelow : J < healthyEquilibrium R c_min) :
    0 < producerProfit R J c_min := by
  unfold producerProfit healthyEquilibrium at *
  rw [lt_div_iff₀ hc] at hbelow
  rw [sub_pos, lt_div_iff₀ hJ]; linarith

Dependency Graph

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:156

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file