Documentation

Lean 4 Proof

theorem bifurcation_condition {R c_min : ℝ} (hc : 0 < c_min) :
    0 < healthyEquilibrium R c_min ↔ 0 < R := by
  unfold healthyEquilibrium
  constructor
  · intro h
    by_contra h'
    push_neg at h'
    linarith [div_nonpos_of_nonpos_of_nonneg h' hc.le]
  · intro h
    exact div_pos h hc

Dependency Graph

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:184

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file