theorem
other
other
market_eq_health
No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
42theorem market_eq_health : MarketEquilibrium = HealthEquilibrium := rfl
depends on (2)
Lean names referenced from this declaration's body.
-
HealthEquilibrium
in IndisputableMonolith.CrossDomain.JEquilibriumUniversality
decl_use
-
MarketEquilibrium
in IndisputableMonolith.CrossDomain.JEquilibriumUniversality
decl_use