Simultaneous shifts: Ibn Taymiyyah's law of price

Proved

SupplyDemand.ibn_taymiyyah

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$ and $D_1,D_2$ demand curves strictly decreasing on $I$ . Let $(p_1,q_1)$ be a market equilibrium of $(S_1,D_1)$ and $(p_2,q_2)$ a market equilibrium of $(S_2,D_2)$ , with $p_1,p_2\in I$ . Then:

if demand increases ( $D_1<D_2$ on $I$ ) while supply decreases ( $S_2<S_1$ on $I$ ), then $p_1<p_2$ ;
if demand decreases ( $D_2<D_1$ on $I$ ) while supply increases ( $S_1<S_2$ on $I$ ), then $p_2<p_1$ .

This is the precise form of the quotation "If desire for goods increases while its availability decreases, its price rises. On the other hand, if availability of the good increases and the desire for it decreases, the price comes down." Nothing is asserted about the quantity, whose direction is undetermined.

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 ibn_taymiyyah (I : Set ℝ) (S₁ S₂ D₁ D₂ : ℝ → ℝ)
    (hS₁ : StrictMonoOn S₁ I) (hS₂ : StrictMonoOn S₂ I)
    (hD₁ : StrictAntiOn D₁ 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 ∈ I, D₁ p < D₂ p) → (∀ p ∈ I, S₂ p < S₁ p) → p₁ < p₂) ∧
    ((∀ p ∈ I, D₂ p < D₁ p) → (∀ p ∈ I, S₁ p < S₂ p) → p₂ < p₁) := 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 "History" (quotation of Ibn Taymiyyah)

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$ , all functions $S_1,S_2,D_1,D_2:\mathbb R\to\mathbb R$ with $S_1,S_2$ strictly increasing on $I$ and $D_1,D_2$ strictly decreasing on $I$ , and all reals $p_1,q_1,p_2,q_2$ with $p_1,p_2\in I$ , $D_1(p_1)=q_1$ , $S_1(p_1)=q_1$ , $D_2(p_2)=q_2$ , $S_2(p_2)=q_2$ , the statement asserts both of the following implications: (a) if $D_1(p)<D_2(p)$ for all $p\in I$ and $S_2(p)<S_1(p)$ for all $p\in I$ , then $p_1<p_2$ ; (b) if $D_2(p)<D_1(p)$ for all $p\in I$ and $S_1(p)<S_2(p)$ for all $p\in I$ , then $p_2<p_1$ . No conclusion about $q_1,q_2$ is drawn.

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