Market supply of upward-sloping firm supplies is upward-sloping

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 type $\iota$, every set $I\subseteq\mathbb R$, every finite set $s$ of elements of $\iota$ that is nonempty, and every family of functions $f_i:\mathbb R\to\mathbb R$ ($i\in\iota$) such that $f_i$ is strictly increasing on $I$ for each $i\in s$ (no condition for $i\notin s$), the function $p\mapsto\sum_{i\in s}f_i(p)$ is strictly increasing on $I$: for $x,y\in I$ with $x<y$, $\sum_{i\in s}f_i(x)<\sum_{i\in s}f_i(y)$.