Documentation

Lean 4 Proof

theorem healthy_eq_positive {R c_min : ℝ}
    (hc : 0 < c_min) (hR : c_min < R) :
    0 < healthyEquilibrium R c_min :=
  div_pos (by linarith) hc

Dependency Graph

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:149

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file