Market demand of downward-sloping individual demands is downward-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 nonempty finite set $s$ of elements of $\iota$, and every family of functions $f_i:\mathbb R\to\mathbb R$ such that $f_i$ is strictly decreasing on $I$ for each $i\in s$, the function $p\mapsto\sum_{i\in s}f_i(p)$ is strictly decreasing on $I$: for $x,y\in I$ with $x<y$, $\sum_{i\in s}f_i(x)>\sum_{i\in s}f_i(y)$.