Documentation

Lean 4 Proof

theorem equilibriumShare_is_shareFunction
    (a cost : Fin J → ℝ) (ρ : ℝ) (j : Fin J) :
    equilibriumShare a cost ρ j =
    shareFunction (fun k => agentFitness a cost ρ k) j := by
  simp only [equilibriumShare, shareFunction]

Dependency Graph

Location

thesis/CESProofs/Foundations/TenWayIdentity.lean:259

Module Section

Ten Views of a Single Object:

In the same file