Proof of Continuity of Projections, Negatives and Differences, and Derivatives on Subintervals

Real numbers are computed with as in The Real Numbers as a Type.

Proof of (i). Every point of $X\times Y$ is an ordered pair $(x,y)$ with $x\in X$ and $y\in Y$, by The Cartesian Product of Two Classes (i) and Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (i). Let $S\subseteq X\times Y$; by Domains and Restrictions of Maps (ii) and Domains and Restrictions of Maps (iii), $\pi_{1}|_{S}:S\to X$ and $\pi_{2}|_{S}:S\to Y$ are maps with $\pi_{1}|_{S}(x,y)=\pi_{1}(x,y)=x$ and $\pi_{2}|_{S}(x,y)=\pi_{2}(x,y)=y$ for $(x,y)\in S$, the values of $\pi_{1}$ and $\pi_{2}$ being those of Projection, Evaluation and Currying Maps (i). Let $(x_{1},y_{1})\in S$ and let $\varepsilon>0$ be real; put $\delta=\varepsilon$. Let $(x_{2},y_{2})\in S$ with $d_{X\times Y}((x_{1},y_{1}),(x_{2},y_{2}))<\delta$. By The Product Metric is a Metric (ii), with $(x_{2},y_{2})$ for $p$ and $(x_{1},y_{1})$ for $q$, and by symmetry of the metric $d_{X\times Y}$ (The Product Metric is a Metric (i) and Metric Space (iv)),

$$d_{X}(x_{2},x_{1})\le d_{X\times Y}((x_{2},y_{2}),(x_{1},y_{1}))=d_{X\times Y}((x_{1},y_{1}),(x_{2},y_{2}))<\varepsilon ,$$

and likewise $d_{Y}(y_{2},y_{1})<\varepsilon$. So $\pi_{1}|_{S}$ and $\pi_{2}|_{S}$ are continuous at $(x_{1},y_{1})$ relative to $S$, and, the point being arbitrary, continuous on $S$, by Continuous Map Between Metric Spaces (ii).

Now let $A\subseteq X$ and let $g:A\to Z$ be continuous on $A$. Then $A\times Y\subseteq X\times Y$, by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (i), and by the above, with $A\times Y$ for $S$, $\pi_{1}|_{A\times Y}:A\times Y\to X$ is continuous on $A\times Y$; its values $\pi_{1}|_{A\times Y}(x,y)=x$ lie in $A$. By Continuity of Identity Maps, Compositions and Reciprocals (ii), with $(X\times Y,d_{X\times Y})$, $(X,d_{X})$, $(Z,d_{Z})$, $A\times Y$, $A$, $\pi_{1}|_{A\times Y}$ and $g$ for its $(X,d_{X})$, $(Y,d_{Y})$, $(Z,d_{Z})$, $A$, $B$, $f$ and $g$, the composite $k=g\circ\pi_{1}|_{A\times Y}:A\times Y\to Z$ is a map with $k(x,y)=g(x)$ for all $x\in A$ and $y\in Y$, and it is continuous on $A\times Y$. Every map $A\times Y\to Z$ with these values equals $k$, by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv).

Proof of (ii). Let $c:S\to\mathbb{R}$ be the constant map with value $-1$ (Maps Formed Pointwise: Constant Maps, Pairs of Values, Maps Applied to Values, and Families of Maps (i)); it is continuous at every point of $S$ relative to $S$, by Continuity of Sums and Products of Real-Valued Functions on a Metric Space (i), and hence continuous on $S$, by Continuous Map Between Metric Spaces (ii). For $z\in\mathbb{R}^{q}$, $(-1)z=-z$, since both have $k$-th component $(-1)z_{k}=-z_{k}$ for every $k\in[q]$, by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iv) and Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iii); and for $z,w\in\mathbb{R}^{q}$, $z-w=z+(-w)$, by Additive Laws for Vectors in $\mathbb{R}^q$ and for Real $p\times q$ Matrices: Group Laws and Rules for Differences (ii). Hence $-x$ is the map $u\mapsto c(u)x(u)$, and $x-y$ is the map $u\mapsto x(u)+(-y)(u)$, by Maps Formed Pointwise from Vector and Matrix Operations (i) and Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv). Let $s_{0}\in S$. If $x$ is continuous at $s_{0}$ relative to $S$, then so is $-x$, by Continuity of Vector- and Matrix-Valued Maps: the Componentwise Criterion, Norms and Algebraic Operations (iv) applied to $c$ and $x$; if moreover $y$ is, then so is $-y$, and therefore so is $x-y$, by Continuity of Vector- and Matrix-Valued Maps: the Componentwise Criterion, Norms and Algebraic Operations (iv) applied to $x$ and $-y$. The matrix case is the same, with Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (iv) and Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (iii) in place of Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iv) and Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iii), entries in place of components, and $A$, $B$ in place of $x$, $y$. The statements for continuity on $S$ follow by applying these at every $s_{0}\in S$, by Continuous Map Between Metric Spaces (ii).

Proof of (iii). Since $a\le c<d\le b$, we have $a<b$, $c,d\in[a,b]$, and, by Basic Facts about Intervals of the Real Line (v) and Basic Facts about Intervals of the Real Line (ii), $[a,b]$ and $[c,d]$ are intervals containing two distinct points with $[c,d]\subseteq[a,b]$. The restriction $x|_{[c,d]}$ is a map $[c,d]\to\mathbb{R}^{q}$ with $x|_{[c,d]}(u)=x(u)$ for $u\in[c,d]$, by Domains and Restrictions of Maps (ii) and Domains and Restrictions of Maps (iii). Let $t\in[c,d]$ and $k\in[q]$. The component map $(x|_{[c,d]})_{k}$ of Component Maps and Entry Maps (i) and the restriction $(x_{k})|_{[c,d]}$ of the component map $x_{k}$ are maps $[c,d]\to\mathbb{R}$ with the same value $x(u)_{k}$ at every $u\in[c,d]$, so they are equal (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv)). As $x$ is differentiable at $t$, $x_{k}$ is differentiable at $t$ relative to $[a,b]$, with derivative $x'(t)_{k}$, by Derivative of a Vector-Valued or Matrix-Valued Map on an Interval (i). By Restriction Stability of Continuity and of the Derivative (ii), with $[a,b]$ for $I$, $[c,d]$ for $J$, $x_{k}$ for $f$ and $t$ for $x$, the map $(x|_{[c,d]})_{k}=(x_{k})|_{[c,d]}$ is differentiable at $t$ relative to $[c,d]$, with derivative $x'(t)_{k}$. As this holds for every $k\in[q]$, $x|_{[c,d]}$ is differentiable at $t$ relative to $[c,d]$, and $(x|_{[c,d]})'(t)$ has $k$-th component $x'(t)_{k}$ for every $k$, by Derivative of a Vector-Valued or Matrix-Valued Map on an Interval (i); so $(x|_{[c,d]})'(t)=x'(t)=(x'|_{[c,d]})(t)$, by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iii) and Domains and Restrictions of Maps (iii). As $t\in[c,d]$ was arbitrary, $x|_{[c,d]}$ is differentiable, by Derivative of a Vector-Valued or Matrix-Valued Map on an Interval (iii), and its derivative map, from Derivative of a Vector-Valued or Matrix-Valued Map on an Interval (iv), and $x'|_{[c,d]}$ are maps $[c,d]\to\mathbb{R}^{q}$ with the same values, so $(x|_{[c,d]})'=x'|_{[c,d]}$ (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv)). The matrix case is the same, with the entry maps $A_{ij}$ of Component Maps and Entry Maps (ii), Derivative of a Vector-Valued or Matrix-Valued Map on an Interval (ii) and Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (iii) in place of the component maps, Derivative of a Vector-Valued or Matrix-Valued Map on an Interval (i) and Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iii).