Documentation

Lean 4 Proof

theorem active_user_free {B R : ℝ} (h : B ≤ R) :
    netUserCost B R ≤ 0 := by
  unfold netUserCost; linarith

Dependency Graph

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:389

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file