An increase in demand raises equilibrium price and quantity

Proved

SupplyDemand.demand_increase

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 strictly increasing on $I$ , and let $D_1,D_2$ be demand curves strictly decreasing on $I$ , with demand increasing from $D_1$ to $D_2$ : $D_1(p)<D_2(p)$ for all $p\in I$ . If $(p_1,q_1)$ is a market equilibrium of $(S,D_1)$ and $(p_2,q_2)$ is a market equilibrium of $(S,D_2)$ , with $p_1,p_2\in I$ , then

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

A right shift of the demand curve raises both the equilibrium price and the equilibrium quantity; read with the indices exchanged, a left shift lowers both.

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 demand_increase (I : Set ℝ) (S D₁ D₂ : ℝ → ℝ)
    (hS : StrictMonoOn S I) (hD₁ : StrictAntiOn D₁ I) (hD₂ : StrictAntiOn D₂ I)
    (hshift : ∀ p ∈ I, D₁ p < D₂ p)
    {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 "Demand curve shifts"

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\subseteq\mathbb R$ and all functions $S,D_1,D_2:\mathbb R\to\mathbb R$ such that $S$ is strictly increasing on $I$ , $D_1$ and $D_2$ are each strictly decreasing on $I$ , and $D_1(p)<D_2(p)$ for every $p\in I$ , and for all reals $p_1,q_1,p_2,q_2$ with $p_1,p_2\in I$ , $D_1(p_1)=q_1$ , $S(p_1)=q_1$ , $D_2(p_2)=q_2$ , $S(p_2)=q_2$ , the statement asserts the strict inequalities $p_1<p_2$ and $q_1<q_2$ . The supply curve is the same function in both equilibria. No existence of equilibria is assumed or asserted.

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