avewright/proofwiki-math huggingface dataset:
Theorem: Set of Points for which Measurable Function is Real-Valued is Measurable

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $f: X \to \overline \R$ be a $\Sigma$-measurable.
Then: 
:$\set {x \in X : \map f x \in \R}$ is $\Sigma$-measurable.

Proof:
Since $f$ is $\Sigma$-measurable, we have that: 
:for all $n \in \N$ the set $\set {x \in X : \map f x \le n}$ is $\Sigma$-measurable
and:
:for all $n \in \N$ the set $\set {x \in X : -n \le \map f x}$ is $\Sigma$-measurable.
From $\sigma$-Algebra Closed under Countable Intersection, we have: 
:$\set {x \in X : -n \le \map f x \le n} = \set {x \in X : \map f x \le n} \cap \set {x \in X : -n \le \map f x}$ is $\Sigma$-measurable.
Since $\sigma$-algebras are closed under countable union, we also have: 
:$\ds \bigcup_{n \mathop = 1}^\infty \set {x \in X : -n \le \map f x \le n}$ is $\Sigma$-measurable.
We will finally show that: 
:$\ds \set {x \in X : \map f x \in \R} = \bigcup_{n \mathop = 1}^\infty \set {x \in X : -n \le \map f x \le n}$
which gives the claim.
If $x \in X$ has $\map f x \in \R$, then we have: 
:$-\paren {\floor {\size {\map f x} } + 1} \le \map f x \le \floor {\size {\map f x} } + 1$
with:
:$\floor {\size {\map f x} } + 1 \in \N$
So:
:$\ds x \in \bigcup_{n \mathop = 1}^\infty \set {x \in X : -n \le \map f x \le n}$
Now, let: 
:$\ds x \in \bigcup_{n \mathop = 1}^\infty \set {x \in X : -n \le \map f x \le n}$
Then: 
:$-n \le \map f x \le n$
for some $n \in \N$, so certainly: 
:$\map f x \in \R$
So we have: 
:$\ds \set {x \in X : \map f x \in \R} = \bigcup_{n \mathop = 1}^\infty \set {x \in X : -n \le \map f x \le n}$
and hence the claim.
{{qed}}
Category:Measurable Sets
Category:Measurable Functions
Category:Set of Points for which Measurable Function is Real-Valued is Measurable
8jd04151zq9fz3rjarm8a898r10mj6u
Theorem: Set of Points for which Measurable Function is Real-Valued is Measurable/Corollary

:$\set {x \in X : \size {\map f x} = +\infty}$ is $\Sigma$-measurable.

Proof:
We have: 
:$\set {x \in X : \size {\map f x} = +\infty} = X \setminus \set {x \in X : \map f x \in \R}$
From Set of Points for which Measurable Function is Real-Valued is Measurable, we have: 
:$\set {x \in X : \map f x \in \R}$ is $\Sigma$-measurable.
Since $\sigma$-algebras are closed under complementation, we have that: 
:$\set {x \in X : \size {\map f x} = +\infty}$ is $\Sigma$-measurable.
{{qed}}
Category:Set of Points for which Measurable Function is Real-Valued is Measurable
l4jd64uifa7hkusi0vwufjp2mup1inl
Theorem: Image of Projection in Plane

Let $M$ and $N$ be distinct lines in the plane.
:420px
Let $\pr_{M, N}$ be the '''projection on $M$ along $N$''':
:$\forall x \in \R^2: \map {\pr_{M, N} } x =$ the intersection of $M$ with the line through $x$ parallel to $N$.
Then $M$ is the image of $\pr_{M, N}$.

Proof:
Let $x \in \R^2$ be arbitrary.
By definition, the image of $x$ is the intersection of $M$ with the line through $x$ parallel to $N$.
Therefore $\map {\pr_{M, N} } x \in M$.
Hence:
:$\Img {\pr_{M, N} } \subseteq M$.
Now consider $y \in M$.
By Playfair's axiom there exists exactly one straight line $L$ parallel to $N$ passing through $y$.
Hence $y$ is the image of every point on $L$.
As $y$ is arbitrary, it follows that each point on $M$ is the image of some straight line in $\R^2$ under $\pr_{M, N}$.
That is:
:$M \subseteq \Img {\pr_{M, N} }$
The result follows by definition of set equality.
{{qed}}
Theorem: Kernel of Projection in Plane between Lines passing through Origin

Let $M$ and $N$ be distinct lines in the plane both of which pass through the origin $O$.
Let $\pr_{M, N}$ be the '''projection on $M$ along $N$''':
:$\forall x \in \R^2: \map {\pr_{M, N} } x =$ the intersection of $M$ with the line through $x$ parallel to $N$.
Then $N$ is the kernel of $\pr_{M, N}$.
{{explain|As the kernel is a concept defined in relation to a homomorphism, it needs to be clarified what homomorphism is being considered.}}

Proof:
Let $\LL$ be the straight line through $x$ which is parallel to $N$.
Let $\map {\pr_{M, N} } x = \tuple {0, 0}$.
By definition, $\map {\pr_{M, N} } x$ is the intersection of $M$ with $\LL$.
However, as $\map {\pr_{M, N} } x = \tuple {0, 0}$, it follows that $\LL$ is coincident with $N$.
Hence the result.
{{qed}}
Theorem: Fixed Points of Projection in Plane

Let $M$ and $N$ be distinct lines in the plane.
:420px
Let $\pr_{M, N}$ be the '''projection on $M$ along $N$''':
:$\forall x \in \R^2: \map {\pr_{M, N} } x =$ the intersection of $M$ with the line through $x$ parallel to $N$.
Then $M$ is the set of fixed points of $\pr_{M, N}$ in the sense that:
:$x \in M$
{{iff}}:
:$\map {\pr_{M, N} } x = x$

Proof:
=== Sufficient Condition ===
Let $x \in M$.
Let $\LL$ be the straight line through $x$ which is parallel to $N$.
As $x \in M$ it follows that $x$ is on the intersection of $M$ with $\LL$.
Hence by definition:
:$\map {\pr_{M, N} } x = x$
{{qed|lemma}}
Theorem: Projection in Plane on X-Axis along Y-Axis

Let $\pr_{X, Y}$ denote the '''projection on the $x$-axis along the $y$-axis''':
:$\forall P \in \R^2: \map {\pr_{X, Y} } P =$ the intersection of the $x$-axis with the line through $P$ parallel to the $y$-axis.
Let $P = \tuple {\lambda_1, \lambda_2}$ be an arbitrary point in $\R^2$.
Then:
:$\map {\pr_{X, Y} } {\lambda_1, \lambda_2} = \tuple {\lambda_1, 0}$

Proof:
This is an instance of a '''projection on $M$ along $N$''' where $N$ coincides with the $y$-axis.
Hence it is one of the special cases of Equations defining Projection in Plane: Cartesian:
:$\map {\pr_{M, N} } P = \tuple {\lambda_1, \lambda_1 \tan \theta}$
where $\theta$ is the angle between $M$ and the $x$-axis.
In this case, $M$ is actually coincident with the $x$-axis.
Hence $\theta = 0$ and so from Tangent of Zero:
:$\map {\pr_{X, Y} } P = \tuple {\lambda_1, 0}$
{{qed}}
Theorem: Projection in Plane on Y-Axis along X-Axis

Let $\pr_{Y, X}$ denote the '''projection on the $y$-axis along the $x$-axis''':
:$\forall P \in \R^2: \map {\pr_{Y, X} } P =$ the intersection of the $y$-axis with the line through $P$ parallel to the $x$-axis.
Let $P = \tuple {\lambda_1, \lambda_2}$ be an arbitrary point in $\R^2$.
Then:
:$\map {\pr_{Y, X} } {\lambda_1, \lambda_2} = \tuple {0, \lambda_2}$

Proof:
This is an instance of a '''projection on $M$ along $N$''' where $M$ coincides with the $y$-axis.
Hence it is one of the special cases of Equations defining Projection in Plane: Cartesian:
:$\map {\pr_{M, N} } P = \tuple {0, \lambda_2 - \lambda_1 \tan \phi}$
where $\phi$ is the angle between $N$ and the $x$-axis.
In this case, $N$ is actually coincident with the $x$-axis.
Hence $\phi = 0$ and so from Tangent of Zero:
:$\map {\pr_{X, Y} } P = \tuple {0, \lambda_2}$
{{qed}}
Theorem: Functions A.E. Equal iff Positive and Negative Parts A.E. Equal

Let $\struct {X, \Sigma, \mu}$ be a measure space. 
Let $f, g : X \to \overline \R$ be extended real-valued functions. 
Then $f = g$ $\mu$-almost everywhere {{iff}}:
:$f^+ = g^+$ $\mu$-almost everywhere and $f^- = g^-$ $\mu$-almost everywhere.

Proof:
=== Necessary Condition ===
Suppose that $f = g$ $\mu$-almost everywhere. 
Then there exists a $\mu$-null set $N \subseteq X$ such that: 
:if $x \in X$ has $\map f x \ne \map g x$, then $x \in N$.
From the definition of the positive part, we have: 
:$\map {f^+} x = \max \set {\map f x, 0}$
and:
:$\map {g^+} x = \max \set {\map g x, 0}$
Clearly if $\map f x = \map g x$, we then have $\map {f^+} x = \map {g^+} x$. 
So from Proof by Contraposition, if $\map {f^+} x \ne \map {g^+} x$ for $x \in X$, we have that $\map f x \ne \map g x$.
That is, if $\map {f^+} x \ne \map {g^+} x$, we have $x \in N$, which is $\mu$-null set.
So:
:$f^+ = g^+$ $\mu$-almost everywhere.
From the definition of the negative part, we have:
:$\map {f^-} x = -\min \set {\map f x, 0}$
and:
:$\map {g^-} x = -\min \set {\map g x, 0}$
As before, by contraposition, if $\map {f^-} x \ne \map {g^-} x$ for $x \in X$, we have that $\map f x \ne \map g x$.
So, if $\map {f^-} x \ne \map {g^-} x$, then $x \in N$.
Again, $N$ is $\mu$-null so we also obtain: 
:$f^- = g^-$ $\mu$-almost everywhere.
{{qed|lemma}}
Theorem: A.E. Equal Positive Measurable Functions have Equal Integrals/Corollary 1

Let $f: X \to \overline \R$ be a $\mu$-integrable function.
Let $g: X \to \overline \R$ be $\Sigma$-measurable.
Suppose that $f = g$ almost everywhere.
Then $g$ is also $\mu$-integrable, and:
:$\ds \int f \rd \mu = \int g \rd \mu$

Proof:
From Function Measurable iff Positive and Negative Parts Measurable, we have that: 
:$g^+$, $f^+$, $g^-$ and $f^-$ are all $\Sigma$-measurable.
From Functions A.E. Equal iff Positive and Negative Parts A.E. Equal, we have that: 
:$f^+ = g^+$ and $f^- = g^-$ $\mu$-almost everywhere. 
Since $f^+$ and $g^+$ are positive $\Sigma$-measurable functions that are equal $\mu$-almost everywhere, we have: 
:$\ds \int f^+ \rd \mu = \int g^+ \rd \mu$ 
from A.E. Equal Positive Measurable Functions have Equal Integrals.
Similarly, we have that $f^-$ and $g^-$ are positive $\Sigma$-measurable functions that are equal $\mu$-almost everywhere, and so:
:$\ds \int f^- \rd \mu = \int g^- \rd \mu$
Since $f$ is $\mu$-integrable, we have that: 
:$\ds \int f^+ \rd \mu < \infty$
and:
:$\ds \int f^- \rd \mu < \infty$
Hence: 
:$\ds \int g^+ \rd \mu < \infty$
and:
:$\ds \int g^- \rd \mu < \infty$
So $g$ is $\mu$-integrable.
We also have: 
{{begin-eqn}}
{{eqn | l = \int g \rd \mu
      | r = \int g^+ \rd \mu - \int g^- \rd \mu
      | c = {{Defof|Integral of Measure-Integrable Function}}
}}
{{eqn | r = \int f^+ \rd \mu - \int f^- \rd \mu
}}
{{eqn | r = \int f \rd \mu
      | c = {{Defof|Integral of Measure-Integrable Function}}
}}
{{end-eqn}}
{{qed}}
Category:A.E. Equal Positive Measurable Functions have Equal Integrals
odh9y3yphgxpob1xufep4vkb6calgje
Theorem: Constant Function is Measurable

Let $\struct {X, \Sigma, \mu}$ be a measure space. 
Let $f : X \to \overline \R$ be a constant extended real-valued function.
That is, there exists $c \in \overline \R$ such that: 
:$\map f x = c$ for all $x \in X$. 
Then $f$ is $\Sigma$-measurable.

Proof:
By the definition of a $\Sigma$-measurable function, we aim to show that: 
:$\set {x \in X : \map f x \le r}$ is $\Sigma$-measurable for each $r \in \R$.
First suppose that $\size c < \infty$. 
Note that there are no $x \in X$ such that $\map f x < c$.
So for $r < c$, we have: 
:$\set {x \in X : \map f x \le r} = \O$
From $\sigma$-Algebra Contains Empty Set, we then have: 
:$\set {x \in X : \map f x \le r} \in \Sigma$ if $r < c$. 
Since for all $x \in X$ we have $\map f x = c$, we also have $\map f x \le c$ for all $x \in X$.
So, if $r \ge c$:
:$\set {x \in X : \map f x \le r} = X$
From the definition of a $\sigma$-algebra, we then have: 
:$\set {x \in X : \map f x \le r} \in \Sigma$ if $r \ge c$. 
So:
:$\set {x \in X : \map f x \le r} \in \Sigma$ for all $r \in \R$
which was the demand.
Now suppose that $c = \infty$. 
Then we have: 
:$\map f x \ge r$
for all $x \in X$ and $r \in \R$. 
So:
:$\set {x \in X : \map f x \le r} = \O$
for each $r \in \R$. 
From $\sigma$-Algebra Contains Empty Set we have $\O \in \Sigma$, so:
:$\set {x \in X : \map f x \le r} \in \Sigma$ for all $r \in \R$.
Now suppose that $c = -\infty$. 
Then we have: 
:$\map f x \le r$
for all $x \in X$ and $r \in \R$.
So:
:$\set {x \in X : \map f x \le r} = X$
for each $r \in \R$. 
From the definition of a $\sigma$-algebra, we have that $X \in \Sigma$, so:
:$\set {x \in X : \map f x \le r} \in \Sigma$ for all $r \in \R$.
{{qed}}
Theorem: Constant Function is Measurable

Let $\struct {X, \Sigma, \mu}$ be a measure space. 
Let $f : X \to \overline \R$ be a constant extended real-valued function.
That is, there exists $c \in \overline \R$ such that: 
:$\map f x = c$ for all $x \in X$. 
Then $f$ is $\Sigma$-measurable.

Proof:
First, suppose that $\size c < \infty$. 
From Characteristic Function of Universe, we can write: 
:$\map f x = c \map {\chi_X} x$
for each $x \in X$.
From the definition of a $\sigma$-algebra, we have: 
:$X \in \Sigma$
So: 
:$f$ is a simple function.
Then, from Simple Function is Measurable, we have: 
:$f$ is $\Sigma$-measurable. 
Now suppose that $c = \infty$. 
For each $n \in \N$, define $f_n : X \to \R$ by: 
:$\map {f_n} x = n$
for each $x \in X$. 
Then: 
:$\ds \map f x = \lim_{n \mathop \to \infty} \map {f_n} x$ 
for each $x \in X$.
We have shown that each $f_n$ is $\Sigma$-measurable for each $n \in \N$, so this is the limit of $\Sigma$-measurable functions.
So, by Pointwise Limit of Measurable Functions is Measurable:
:$f$ is $\Sigma$-measurable in this case. 
Now suppose that $c = -\infty$.
For each $n \in \N$, define $g_n : X \to \R$ by: 
:$\map {g_n} x = -n$
for each $x \in X$. 
Then: 
:$\ds \map f x = \lim_{n \mathop \to \infty} \map {g_n} x$ 
for each $x \in X$.
We have shown that each $g_n$ is $\Sigma$-measurable for each $n \in \N$, so this is the limit of $\Sigma$-measurable functions.
So, by Pointwise Limit of Measurable Functions is Measurable:
:$f$ is $\Sigma$-measurable in this case.
{{qed}}
Theorem: Equations defining Projection in Plane/Cartesian

Let $M$ and $N$ be distinct lines in the plane, both of which pass through the origin.
Let the angle between $M$ and the $x$-axis be $\theta$.
Let the angle between $N$ and the $x$-axis be $\phi$.
Let $\pr_{M, N}$ be the '''projection on $M$ along $N$''':
:$\forall P \in \R^2: \map {\pr_{M, N} } P =$ the intersection of $M$ with the line through $P$ parallel to $N$.
Let $P = \tuple {x, y}$ be an arbitrary point in the plane.
Then:
:$\map {\pr_{M, N} } P = \begin {cases} 
\tuple {0, y - x \tan \phi} & : \theta = \dfrac \pi 2 \\
\tuple {x, x \tan \theta} & : \phi = \dfrac \pi 2 \\
\tuple {\dfrac {x \tan \phi} {\tan \phi - \tan \theta} - \dfrac y {\tan \phi - \tan \theta}, \dfrac {y \tan \theta} {\tan \theta - \tan \phi} - \dfrac {x \tan \theta \tan \phi} {\tan \theta - \tan \phi} } & : \text {otherwise} 
\end {cases}$

Proof:
Let $P = \tuple {x_1, y_1} \in \R^2$ be arbitrary.
:540px
From Equation of Straight Line in Plane: Slope-Intercept Form, we can express $M$ and $N$ as follows:
{{begin-eqn}}
{{eqn | q = M
      | l = y
      | r = m x
}}
{{eqn | q = N
      | l = y
      | r = n x
}}
{{end-eqn}}
where:
{{begin-eqn}}
{{eqn | l = m
      | r = \tan \theta
}}
{{eqn | l = n
      | r = \tan \phi
}}
{{end-eqn}}
Let $\pr_{M, N}$ map $P = \tuple {x_1, y_1}$ onto $P' = \tuple {x_2, y_2}$.
From Equation of Straight Line in Plane: Point-Slope Form, $PP'$ can be expressed as:
:$y - y_1 = n \paren {x - x_1}$
This holds also for $\tuple {x_2, y_2}$, and so:
{{begin-eqn}}
{{eqn | l = y_2 - y_1
      | r = n \paren {x_2 - x_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = n x_2
      | r = y_2 - y_1 + n x_1
      | c = 
}}
{{eqn | r = m x_2 - y_1 + n x_1
      | c = as $\tuple {x_2, y_2} \in M$
}}
{{eqn | ll= \leadsto
      | l = \paren {n - m} x_2
      | r = n x_1 - y_1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x_2
      | r = \dfrac {n x_1} {n - m} - \dfrac {y_1} {n - m}
      | c = 
}}
{{end-eqn}}
Similarly:
{{begin-eqn}}
{{eqn | l = y_2 - y_1
      | r = n \paren {x_2 - x_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {y_2} n
      | r = x_2 - x_1 + \dfrac {y_1} n
      | c = 
}}
{{eqn | r = \dfrac {y_2} m - x_1 + \dfrac {y_1} n
      | c = as $\tuple {x_2, y_2} \in M$
}}
{{eqn | ll= \leadsto
      | l = \paren {\dfrac 1 n - \dfrac 1 m} y_2
      | r = \dfrac {y_1} n - x_1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y_2
      | r = \dfrac {m y_1} {m - n} - \dfrac {m n x_1} {m - n}
      | c = 
}}
{{end-eqn}}
The result follows by substituting for $m$ and $n$.
{{qed|lemma}}
Theorem: Bound for Positive Part of Pointwise Sum of Functions

Let $X$ be a set.
Let $f, g : X \to \overline \R$ be extended real-valued function.
Suppose that the pointwise sum $f + g$ is well-defined, that is: 
:there exists no $x \in X$ such that $\set {\map f x, \map g x} = \set {\infty, -\infty}$.
Then: 
:$\paren {f + g}^+ \le f^+ + g^+$
where $\paren {f + g}^+$, $f^+$ and $g^+$ denote the positive parts of $f + g$, $f$ and $g$ respectively.

Proof:
Let $x \in X$. 
From the definition of the positive part, we have: 
:$\map {f^+} x = \max \set {\map f x, 0}$
and:
:$\map {g^+} x = \max \set {\map g x, 0}$
Suppose first that $\map f x$ and $\map g x$ are finite. 
From Maximum Function in terms of Absolute Value, we then have: 
:$\ds \map {f^+} x = \frac {\map f x + \size {\map f x} } 2$
and:
:$\ds \map {g^+} x = \frac {\map g x + \size {\map g x} } 2$
We then have: 
{{begin-eqn}}
{{eqn	| l = \map {\paren {f + g}^+} x
	| r = \max \set {\map f x + \map g x, 0}
	| c = {{Defof|Positive Part}}
}}
{{eqn	| r = \frac {\paren {\map f x + \map g x} + \size {\map f x + \map g x} } 2
	| c = Maximum Function in terms of Absolute Value
}}
{{eqn	| o = \le
	| r = \frac {\paren {\map f x + \map g x} + \size {\map f x} + \size {\map g x} } 2
	| c = Triangle Inequality
}}
{{eqn	| r = \frac {\map f x + \size {\map f x} } 2 + \frac {\map g x + \size {\map g x} } 2
}}
{{eqn	| r = \map {f^+} x + \map {g^+} x
}}
{{end-eqn}}
Now suppose that $\map f x = +\infty$. 
Then $\map g x > -\infty$.
We then have: 
:$\map f x + \map g x = +\infty$
So:
:$\map {\paren {f + g}^+} x = +\infty$
and: 
:$\map {f^+} x = +\infty$
So the inequality:
:$\map {\paren {f + g}^+} x \le \map {f^+} x + \map {g^+} x$
holds trivially. 
Swapping $f$ for $g$, we also get the result if $\map g x = +\infty$ and $\map f x > -\infty$. 
Now suppose that $\map f x = -\infty$
Then $\map g x < \infty$.
Then: 
:$\map f x + \map g x = -\infty$
So:
:$\map {\paren {f + g}^+} x = 0$
and: 
:$\map {f^+} x = 0$
We have that: 
:$\map {g^+} x \ge 0$
so: 
:$\map {\paren {f + g}^+} x \le \map {f^+} x + \map {g^+} x$
Swapping $f$ for $g$, we also get the result if $\map g x = -\infty$ and $\map f x < \infty$.
{{qed}}
Category:Positive Parts
fnfj1stm8vuikcbdgsns52uea5o8baw
Theorem: Sequence of P-adic Integers has Convergent Subsequence/Lemma 6

there exists a subsequence $\sequence{y_n}$ of $\sequence{x_n}$:
:for all $n \in \N$, the canonical expansion of $y_n$ begins with the $p$-adic digits $b_j \, \ldots \, b_1 b_0$

Proof:
For any non-empty subset $S$ of $\N$, let $\min S$ denote the smallest element of $S$.
From the Well-Ordering Principle, for any non-empty subset $S$ of $\N$, $\min S$ always exists.
Let $g:\N \to \N$ be the mapping defined by:
:$\map g n = \min \set{n > j : \text{ the canonical expansion of } x_n \text{ begins with the } p \text{-adic digits } b_j \, \ldots \, b_1 b_0}$
Let:
:$n_0 = \min \set{n \in \N : \text{ the canonical expansion of } x_n \text{ begins with the } p \text{-adic digits } b_j \, \ldots \, b_1 b_0}$
From Well-Ordering Principle:
:$g$ and $n_0$ are well-defined
From Principle of Recursive Definition:
:there exists exactly one mapping $r: \N \to \N$ such that:
::$\forall m \in \N: \map r m = \begin{cases}
a & : m = 0 \\
\map g {\map r n} & : m = n + 1
\end{cases}$
It is noted that:
:{{begin-eqn}}
{{eqn | q = \forall n \in \N
      | l = \map r {n + 1}
      | r = \map g {\map r n }
      | c = definition of $r$ 
}}
{{eqn | o = >
      | r = \map r n
      | c = definition of $g$ 
}}
{{end-eqn}}
Hence $r$ is a strictly increasing sequence in $\N$.
For all $n \in \N$, let $m_n = \map r n$.
Then $\sequence{x_{m_n}}$ is a subsequence of $\sequence{x_n}$ by definition.
Let $\sequence{y_n} = \sequence{x_{m_n}}$ and the result follows
{{qed}}
category:Sequence of P-adic Integers has Convergent Subsequence
162gah6z0a79g8ckxx9pmuyp35a03p6
Theorem: Sequence of P-adic Integers has Convergent Subsequence/Lemma 1

there exists a $p$-adic digit $b_0$ such that:
:there exists infinitely many $n \in \N$ such that the canonical expansion of $x_n$ begins with the $p$-adic digit $b_0$

Proof:
=== Case 1 ===
Let there exist $b \in \set{0, 1, \ldots , p - 2}$:
:there exists infinitely many $n \in \N$ such that the canonical expansion of $y_n$ begins with the $p$-adic digits $b$
Let $b_0 = b$ and  the result holds.
{{qed|lemma}}
Theorem: Real Power Function for Positive Integer Power is Continuous

Let $n \in \Z_{\ge 0}$ be a positive integer.
Let $f_n: \R \to \R$ be the real function defined as:
:$\forall x \in \R: \map {f_n} x = x^n$
Then $f_n$ is continuous on $\R$.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\forall x \in \R: f_n$ is continuous on $\R$.
$\map P 0$ is the case:
:$\forall x \in \R: \map {f_0} x = x^0 = 1$
Thus it is seen that $f_0$ is the constant mapping.
It follows from Constant Real Function is Continuous that $f_0$ is continuous on $\R$.
Thus $\map P 0$ is seen to hold.
Theorem: Bound for Negative Part of Pointwise Sum of Functions

Let $X$ be a set. 
Let $f, g : X \to \overline \R$ be extended real-valued function.
Suppose that the pointwise sum $f + g$ is well-defined, that is: 
:there exists no $x \in X$ such that $\set {\map f x, \map g x} = \set {\infty, -\infty}$.
Then: 
:$\paren {f + g}^- \le f^- + g^-$
where $\paren {f + g}^-$, $f^-$ and $g^-$ denote the negative parts of $f + g$, $f$ and $g$ respectively.

Proof:
Let $x \in X$. 
From the definition of the negative part, we have: 
:$\map {f^-} x = -\min \set {\map f x, 0}$
and:
:$\map {g^-} x = -\min \set {\map g x, 0}$
Suppose first that $\map f x$ and $\map g x$ are finite.
From Minimum Function in terms of Absolute Value, we then have:
:$\ds \map {f^-} x = \frac {\size {\map f x} - \map f x} 2$
and:
:$\ds \map {g^-} x = \frac {\size {\map g x} - \map g x} 2$
We then have: 
{{begin-eqn}}
{{eqn	| l = \map {\paren {f + g}^-} x
	| r = -\min \set {\map f x + \map g x, 0}
	| c = {{Defof|Negative Part}}
}}
{{eqn	| r = \frac {\size {\map f x + \map g x} - \paren {\map f x + \map g x} } 2
	| c = Minimum Function in terms of Absolute Value
}}
{{eqn	| o = \le
	| r = \frac {\size {\map f x} + \size {\map g x} - \paren {\map f x + \map g x} } 2
	| c = Triangle Inequality
}}
{{eqn	| r = \frac {\size {\map f x} - \map f x} 2 + \frac {\size {\map g x} - \map g x} 2
}}
{{eqn	| r = \map {f^-} x + \map {g^-} x
}}
{{end-eqn}}
Now suppose that $\map f x = +\infty$. 
Then $\map g x > -\infty$.
We then have:
:$\map f x + \map g x = +\infty$
So:
:$\map {\paren {f + g}^-} x = 0$
and:
:$\map {f^-} x = 0$
Since: 
:$\map {g^-} x \ge 0$
we have that: 
:$\map {\paren {f + g}^-} x \le \map {f^-} x + \map {g^-} x$
Swapping $f$ for $g$, we also get the result if $\map g x = +\infty$ and $\map f x > -\infty$.
Now suppose that $\map f x = -\infty$
Then $\map g x < \infty$.
Then: 
:$\map f x + \map g x = -\infty$
So:
:$\map {\paren {f + g}^-} x = \infty$
and:
:$\map {f^-} x = \infty$
So the inequality: 
:$\map {\paren {f + g}^-} x \le \map {f^-} x + \map {g^-} x$
holds trivially. 
Swapping $f$ for $g$, we also get the result if $\map g x = -\infty$ and $\map f x < \infty$.
{{qed}}
Category:Negative Parts
58mj1odx96hctxs1dp2u8h71sdrhbd4
Theorem: Real Polynomial Function is Differentiable

Let $n \in \Z_{\ge 0}$ be a positive integer.
Let $f_n: \R \to \R$ be a real polynomial function.
Then $f_n$ is differentiable over $\R$.

Proof:
Let $f_n$ be an arbitrary real polynomial function of degree $n$.
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$f_n$ is differentiable over $\R$.
$\map P 0$ is the case $f_0$, where $f_0$ is of zero degree.
Such a real polynomial function is a constant function.
From Derivative of Constant we have that $f_0$ is differentiable over $\R$.
Thus $\map P 0$ is seen to hold.