Documentation

Lean 4 Proof

theorem log_exceeds_purchase {V_purchased V_curriculum : ℝ}
    (hV : 0 < V_curriculum) :
    V_purchased < contextLogValue V_purchased V_curriculum := by
  unfold contextLogValue; linarith

Dependency Graph

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:363

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file