Uniqueness of the market equilibrium

Proved

SupplyDemand.equilibrium_unique

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

economicsmicroeconomicssupply-and-demand

Let $I\subseteq\mathbb R$ be a set of admissible prices, let $S$ be a supply curve that is strictly increasing on $I$ , and let $D$ be a demand curve that is strictly decreasing on $I$ . If $(p_1,q_1)$ and $(p_2,q_2)$ are both market equilibria of $(S,D)$ with $p_1,p_2\in I$ , then

p_1=p_2\quad\text{and}\quad q_1=q_2.

So, for upward-sloping supply and downward-sloping demand, the equilibrium is "the" intersection of the two curves, as the source describes it.

Formalization Note Curves are functions $\mathbb R\to\mathbb R$ ; the slope assumptions are imposed on an arbitrary set $I$ of admissible prices, and all equilibrium prices are assumed to lie in $I$ .

Preamble

import Mathlib
import Definitions.Def_SupplyDemand_Model

Formal statement

namespace SupplyDemand

theorem equilibrium_unique (I : Set ℝ) (S D : ℝ → ℝ)
    (hS : StrictMonoOn S I) (hD : StrictAntiOn D I)
    {p₁ q₁ p₂ q₂ : ℝ} (hp₁ : p₁ ∈ I) (hp₂ : p₂ ∈ I)
    (h₁ : IsEquilibrium S D p₁ q₁) (h₂ : IsEquilibrium S D p₂ q₂) :
    p₁ = p₂ ∧ q₁ = q₂ := by sorry

end SupplyDemand

Source

Wikipedia, "Supply and demand", revision 1378800284, https://en.wikipedia.org/w/index.php?title=Supply_and_demand&oldid=1378800284, section "Equilibrium" and "Market equilibrium"

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Disclosure — NON-BLIND read-back. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement it describes, with full knowledge of the source article and of the intended meaning. It is not independent, blind testimony and must not be mistaken for one. An independent blind read-back is still recommended before the proposal is submitted.

For every set $I$ of real numbers, every pair of functions $S,D:\mathbb R\to\mathbb R$ such that $S$ is strictly increasing on $I$ (for $x,y\in I$ , $x<y$ implies $S(x)<S(y)$ ) and $D$ is strictly decreasing on $I$ ( $x<y$ in $I$ implies $D(x)>D(y)$ ), and all reals $p_1,q_1,p_2,q_2$ with $p_1\in I$ , $p_2\in I$ , $D(p_1)=q_1$ , $S(p_1)=q_1$ , $D(p_2)=q_2$ , $S(p_2)=q_2$ , the statement asserts $p_1=p_2$ and $q_1=q_2$ . Nothing is assumed about existence of such points; $I$ may be empty (then the hypotheses $p_1\in I$ cannot hold) or any other set.

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph