An increase in supply lowers equilibrium price and raises quantity

Proved

SupplyDemand.supply_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_1,S_2$ be supply curves strictly increasing on $I$ , with supply increasing from $S_1$ to $S_2$ : $S_1(p)<S_2(p)$ for all $p\in I$ , and let $D$ be a demand curve strictly decreasing on $I$ . If $(p_1,q_1)$ is a market equilibrium of $(S_1,D)$ and $(p_2,q_2)$ is a market equilibrium of $(S_2,D)$ , with $p_1,p_2\in I$ , then

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

After a supply shift, price and quantity move in opposite directions; read with the indices exchanged, a left shift raises the price and lowers the quantity.

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 supply_increase (I : Set ℝ) (S₁ S₂ D : ℝ → ℝ)
    (hS₁ : StrictMonoOn S₁ I) (hS₂ : StrictMonoOn S₂ I) (hD : StrictAntiOn D I)
    (hshift : ∀ p ∈ I, S₁ p < S₂ 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 "Supply 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_1,S_2,D:\mathbb R\to\mathbb R$ such that $S_1$ and $S_2$ are each strictly increasing on $I$ , $D$ is strictly decreasing on $I$ , and $S_1(p)<S_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(p_1)=q_1$ , $S_1(p_1)=q_1$ , $D(p_2)=q_2$ , $S_2(p_2)=q_2$ , the statement asserts $p_2<p_1$ (the second price is strictly smaller) and $q_1<q_2$ (the second quantity is strictly larger). The demand 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