avewright/proofwiki-math huggingface dataset:
Theorem: Distribution Function of Finite Borel Measure is Right-Continuous

Let $\mu$ be a finite Borel measure on $\R$.
Let $F_\mu$ be the distribution function of $\mu$.
Then $F_\mu$ is right-continuous.

Proof:
From Monotonic Sequential Right-Continuity is Equivalent to Right-Continuity in the Reals, it suffices to show that: 
:for all monotone sequences $\sequence {x_n}_{n \mathop \in \N}$, with $x_n > x$ for each $n$, that converge to $x$ we have:
::$\ds \map {F_\mu} x = \lim_{n \mathop \to \infty} \map {F_\mu} {x_n}$
Now let $\sequence {x_n}_{n \mathop \in \N}$ be a monotone sequence with $x_n > x$ for each $n \in \N$ and $x_n \to x$.
Then $\sequence {\hointl {-\infty} {x_n} }_{n \mathop \in \N}$ is a decreasing sequence of sets.
Then from Limit of Decreasing Sequence of Unbounded Below Closed Intervals, we have: 
:$\ds \bigcap_{n \mathop = 1}^\infty \hointl {-\infty} {x_n} = \hointl {-\infty} x$
Since $\mu$ is finite, we have: 
:$\map \mu {\hointl {-\infty} {x_1} } < \infty$
so Measure of Limit of Decreasing Sequence of Measurable Sets is admissable and gives: 
:$\ds \map \mu {\bigcap_{n \mathop = 1}^\infty \hointl {-\infty} {x_n} } = \lim_{n \mathop \to \infty} \map \mu {\hointl {-\infty} {x_n} }$
That is: 
:$\ds \map \mu {\bigcap_{n \mathop = 1}^\infty \hointl {-\infty} {x_n} } = \lim_{n \mathop \to \infty} \map {F_\mu} {x_n}$
so:
:$\ds \map \mu {\hointl {-\infty} x} = \lim_{n \mathop \to \infty} \map {F_\mu} {x_n}$
Hence: 
:$\ds \map {F_\mu} x = \lim_{n \mathop \to \infty} \map {F_\mu} {x_n}$
Since the sequence $\sequence {x_n}_{n \mathop \in \N}$ was arbitrary, we have: 
:$F_\mu$ is right-continuous.
from Monotonic Sequential Right-Continuity is Equivalent to Right-Continuity in the Reals.
{{qed}}
Theorem: Limit of Distribution Function of Finite Borel Measure at Negative Infinity

Let $\mu$ be a finite Borel measure on $\R$.
Let $F_\mu$ be the distribution function of $\mu$.
Then:
:$\ds \lim_{x \mathop \to -\infty} \map {F_\mu} x = 0$

Proof:
From Sequential Characterisation of Limit at Minus Infinity of Real Function: Corollary, we aim to show that: 
:for all decreasing real sequences $\sequence {x_n}_{n \mathop \in \N}$ with $x_n \to -\infty$ we have $\ds \lim_{n \mathop \to \infty} \map {F_\mu} {x_n} = 0$.
Since $\sequence {x_n}_{n \mathop \in \N}$ is decreasing, we have: 
:the sequence $\sequence {\hointl {-\infty} {x_n} }_{n \mathop \in \N}$ is decreasing.
From Limit of Decreasing Sequence of Unbounded Below Closed Intervals with Endpoint Tending to Negative Infinity:
:$\ds \bigcap_{n \mathop = 1}^\infty \hointl {-\infty} {x_n} = \O$
Further, since $\mu$ is a finite measure, we have: 
:$\ds \map \mu {\hointl {-\infty} {x_1} } < \infty$
So Measure of Limit of Decreasing Sequence of Measurable Sets is admissible, and gives: 
:$\ds \map \mu {\bigcap_{n \mathop = 1}^\infty \hointl {-\infty} {x_n} } = \lim_{n \mathop \to \infty} \map {F_\mu} {x_n}$
Since: 
:$\ds \bigcap_{n \mathop = 1}^\infty \hointl {-\infty} {x_n} = \O$
we have: 
:$\ds \map \mu {\bigcap_{n \mathop = 1}^\infty \hointl {-\infty} {x_n} } = 0$
from Empty Set is Null Set.
So:
:$\ds \lim_{n \mathop \to \infty} \map {F_\mu} {x_n} = 0$
Since the sequence $\sequence {x_n}_{n \mathop \in \N}$ was arbitrary, we have: 
:$\ds \lim_{x \mathop \to -\infty} \map {F_\mu} x = 0$
by Sequential Characterisation of Limit at Minus Infinity of Real Function: Corollary.
{{qed}}
Theorem: Properties of Limit at Infinity of Real Function/Sum Rule

Let $a \in \R$. 
Let $f, g : \hointr a \infty \to \R$ be real functions such that: 
:$\ds \lim_{x \mathop \to \infty} \map f x = L_1$
and:
:$\ds \lim_{x \mathop \to \infty} \map g x = L_2$
where $\ds \lim_{x \mathop \to \infty}$ denotes the limit at $+\infty$.
Then: 
:$\ds \lim_{x \mathop \to \infty} \paren {\map f x + \map g x}$ exists
with:
:$\ds \lim_{x \mathop \to \infty} \paren {\map f x + \map g x} = L_1 + L_2$

Proof:
Since: 
:$\ds \lim_{x \mathop \to \infty} \map f x = L_1$
given $\epsilon > 0$, we can find $M_1 \ge 0$ such that: 
:$\ds \size {\map f x - L_1} < \frac \epsilon 2$ for $x \ge M_1$
Since: 
:$\ds \lim_{x \mathop \to \infty} \map g x = L_2$
we can find $M_2 \ge 0$ such that: 
:$\ds \size {\map f x - L_2} < \frac \epsilon 2$ for $x \ge M_2$.
Let:
:$M = \max \set {M_1, M_2}$
Then, for $x \ge M$, we have: 
{{begin-eqn}}
{{eqn	| l = \size {\paren {\map f x + \map g x} - \paren {L_1 + L_2} }
		| r = \size {\paren {\map f x - L_1} + \paren {\map g x - L_2} }
}}
{{eqn	| o = \le
		| r = \size {\map f x - L_1} + \size {\map g x - L_2}
		| c = Triangle Inequality for Real Numbers
}}
{{eqn	| o = <
		| r = \frac \epsilon 2 + \frac \epsilon 2
}}
{{eqn	| r = \epsilon
}}
{{end-eqn}}
Since $\epsilon$ was arbitrary, we have:
:$\ds \lim_{x \mathop \to \infty} \paren {\map f x + \map g x} = L_1 + L_2$
{{qed}}
Category:Properties of Limit at Infinity of Real Function
lkp6caaaut7arbitmt9oy1ihu7z1r2j
Theorem: Properties of Limit at Infinity of Real Function/Multiple Rule

Let $a, \alpha \in \R$. 
Let $f : \hointr a \infty \to \R$ be a real function such that: 
:$\ds \lim_{x \mathop \to \infty} \map f x = L$
where $\ds \lim_{x \mathop \to \infty}$ denotes the limit at $+\infty$.
Then: 
:$\ds \lim_{x \mathop \to \infty} \paren {\alpha \map f x}$ exists
with:
:$\ds \lim_{x \mathop \to \infty} \paren {\alpha \map f x} = \alpha L$

Proof:
If $\alpha = 0$, the result follows from Limit of Constant Function: Limit at $\infty$.
Otherwise, since: 
:$\ds \lim_{x \mathop \to \infty} \map f x = L$
given $\epsilon > 0$ we can find a real number $M \ge 0$ such that: 
:$\ds \size {\map f x - L} < \frac \epsilon {\size \alpha}$ for $x \ge M$.
Then: 
:$\ds \size {\alpha \map f x - \alpha L} < \epsilon$ for $x \ge M$.
Since $\epsilon$ was arbitrary, we have:
:$\ds \lim_{x \mathop \to \infty} \paren {\alpha \map f x}$ exists
with:
:$\ds \lim_{x \mathop \to \infty} \paren {\alpha \map f x} = \alpha L$
{{qed}}
Category:Properties of Limit at Infinity of Real Function
jy5qnm9u29rh2mwe7396ri3r9h7c81t
Theorem: Properties of Limit at Infinity of Real Function/Combined Sum Rule

Let $a, \alpha, \beta \in \R$. 
Let $f, g : \hointr a \infty \to \R$ be real functions such that: 
:$\ds \lim_{x \mathop \to \infty} \map f x = L_1$
and:
:$\ds \lim_{x \mathop \to \infty} \map g x = L_2$
where $\ds \lim_{x \mathop \to \infty}$ denotes the limit at $+\infty$.
Then: 
:$\ds \lim_{x \mathop \to \infty} \paren {\alpha \map f x + \beta \map g x} = \alpha L_1 + \beta L_2$

Proof:
From Properties of Limit at Positive Infinity of Real Function: Multiple Rule, we have: 
:$\ds \lim_{x \mathop \to \infty} \paren {\alpha \map f x} = \alpha L_1$
and:
:$\ds \lim_{x \mathop \to \infty} \paren {\beta \map f x} = \beta L_2$
From Properties of Limit at Positive Infinity of Real Function: Sum Rule, we have: 
:$\ds \lim_{x \mathop \to \infty} \paren {\alpha \map f x + \beta \map g x} = \alpha L_1 + \beta L_2$
{{qed}}
Category:Properties of Limit at Infinity of Real Function
ab66f70bfxufycgdopoezd7ssprdtib
Theorem: Properties of Limit at Infinity of Real Function/Difference Rule

Let $a \in \R$. 
Let $f, g : \hointr a \infty \to \R$ be real functions such that: 
:$\ds \lim_{x \mathop \to \infty} \map f x = L_1$
and:
:$\ds \lim_{x \mathop \to \infty} \map g x = L_2$
where $\ds \lim_{x \mathop \to \infty}$ denotes the limit at $+\infty$.
Then: 
:$\ds \lim_{x \mathop \to \infty} \paren {\map f x - \map g x} = L_1 - L_2$

Proof:
This follows immediately by plugging $\alpha = 1$ and $\beta = -1$ into the combined sum rule.
{{qed}}
Category:Properties of Limit at Infinity of Real Function
91ovt09v20uyg27b6fh16j2nb1y0dz7
Theorem: Properties of Limit at Infinity of Real Function/Product Rule

Let $a \in \R$. 
Let $f, g : \hointr a \infty \to \R$ be real functions such that: 
:$\ds \lim_{x \mathop \to \infty} \map f x = L_1$
and:
:$\ds \lim_{x \mathop \to \infty} \map g x = L_2$
where $\ds \lim_{x \mathop \to \infty}$ denotes the limit at $+\infty$.
Then: 
:$\ds \lim_{x \mathop \to \infty} \paren {\map f x \map g x} = L_1 L_2$

Proof:
Write: 
{{begin-eqn}}
{{eqn	| l = \size {\map f x \map g x - L_1 L_2}
		| r = \size {\map f x \map g x - L_1 L_2 + L_2 \map f x - L_2 \map f x}
}}
{{eqn	| r = \size {\map f x \paren {\map g x - L_2} + L_2 \paren {\map f x - L_1} }
}}
{{eqn	| o = \le
		| r = \size {\map f x} \size {\map g x - L_2} + \size {L_2} \size {\map f x - L_1}
}}
{{end-eqn}}
Since: 
:$\ds \lim_{x \mathop \to \infty} \map f x = L_1$
there exists a real number $M_1 \ge 0$ such that: 
:$\size {\map f x - {L_1} } < 1$
for $x \ge M_1$.
By the Reverse Triangle Inequality, we then have: 
:$\size {\size {\map f x} - \size {L_1} } < 1$
so that:
:$\size {L_1} - 1 < \size {\map f x} < \size {L_1} + 1$
So we have, for $x \ge M_1$: 
:$\size {\map f x} \size {\map g x - L_2} + \size {L_2} \size {\map f x - L_1} < \paren {\size {L_1} + 1} \size {\map g x - L_2} + \size {L_2} \size {\map f x - L_1}$
Since: 
:$\ds \lim_{x \mathop \to \infty} \map g x = L_2$
given $\epsilon > 0$ we can select a real number $M_2 \ge 0$ such that: 
:$\ds \size {\map g x - L_2} < \frac \epsilon {2 \paren {\size {L_1} + 1} }$ for $x \ge M_2$.
If $L_2 = 0$, we are done, since if $x \ge \max \set {M_1, M_2}$, we have: 
{{begin-eqn}}
{{eqn	| l = \size {\map f x \map g x}
		| o = <
		| r = \paren {\size {L_1} + 1} \size {\map g x - L_2}
}}
{{eqn	| o = <
		| r = \paren {\size {L_1} + 1} \paren {\frac \epsilon {2 \paren {\size {L_1} + 1} } }
}}
{{eqn	| r = \frac \epsilon 2
}}
{{end-eqn}}
Then since $\epsilon$ was arbitrary, we then have: 
:$\ds \lim_{x \mathop \to \infty} \paren {\map f x \map g x} = 0$
Now suppose that $L_2 \ne 0$. 
Since: 
:$\ds \lim_{x \mathop \to \infty} \map f x = L_1$
given $\epsilon > 0$ we can pick a real number $M_3 \ge 0$ such that: 
:$\ds \size {\map f x - L_1} < \frac \epsilon {2 \size {L_2} }$
Let:
:$M = \max \set {M_1, M_2, M_3}$
Then, for $x \ge M$, we have: 
{{begin-eqn}}
{{eqn	| l = \paren {\size {L_1} + 1} \size {\map g x - L_2} + \size {L_2} \size {\map f x - L_1}
		| o = <
		| r = \paren {\size {L_1} + 1} \paren {\frac \epsilon {2 \paren {\size {L_1} + 1} } } + \size {L_2} \paren {\frac \epsilon {2 \size {L_2} } }
}}
{{eqn	| r = \frac \epsilon 2 + \frac \epsilon 2
}}
{{eqn	| r = \epsilon
}}
{{end-eqn}}
{{qed}}
Category:Properties of Limit at Infinity of Real Function
rtd9tdlfbig191ny0tcim9bax6od4s7
Theorem: Properties of Limit at Minus Infinity of Real Function/Relation with Limit at Infinity

Let $a \in \R$. 
Let $f : \hointl {-\infty} a \to \R$ be a real function.
Then:
:$\ds \lim_{x \mathop \to -\infty} \map f x$ exists {{iff}} $\ds \lim_{x \mathop \to \infty} \map f {-x}$ exists
and in this case:
:$\ds \lim_{x \mathop \to -\infty} \map f x = \lim_{x \mathop \to \infty} \map f {-x}$
where:
:$\ds \lim_{x \mathop \to \infty}$ denotes the limit at $+\infty$
:$\ds \lim_{x \mathop \to -\infty}$ denotes the limit at $-\infty$.

Proof:
Note that: 
:$\ds \lim_{x \mathop \to -\infty} \map f x = L$
{{iff}} given $\epsilon > 0$ we can find real number $M \le 0$ such that: 
:$\size {\map f x - L} < \epsilon$ for $x \le M$. 
This is equivalent to: 
:given $\epsilon > 0$ we can find real number $M \le 0$ such that $\size {\map f x - L} < \epsilon$ for $x \ge -M$.
Since $\epsilon$ was arbitrary and $-M \ge 0$, we have:
:$\ds \lim_{x \mathop \to -\infty} \map f x$ exists {{iff}} $\ds \lim_{x \mathop \to \infty} \map f {-x}$ exists
with: 
:$\ds \lim_{x \mathop \to \infty} \map f x = L = \lim_{x \mathop -\infty} \map f {-x}$
which was the demand.
{{qed}}
Category:Properties of Limit at Minus Infinity of Real Function
6vc0zlutojjk03xcc72muewgn7xl0eo
Theorem: Cowen's Theorem

Let $g$ be a progressing mapping.
Let $x$ be a set.
Let $\powerset x$ denote the power set of $x$.
Let $M_x$ denote the intersection of the $x$-special subsets of $\powerset x$ {{WRT}} $g$.
Let $M$ be the class of all $x$ such that $x \in M_x$.
Then $M$ is minimally superinductive under $g$.

Proof:
=== Lemma $1$ ===
{{:Cowen's Theorem/Lemma 1}}{{qed|lemma}}
=== Lemma $2$ ===
{{:Cowen's Theorem/Lemma 2}}{{qed|lemma}}
=== Lemma $3$ ===
{{:Cowen's Theorem/Lemma 3}}{{qed|lemma}}
=== Lemma $4$ ===
{{:Cowen's Theorem/Lemma 4}}{{qed|lemma}}
=== Lemma $5$ ===
{{:Cowen's Theorem/Lemma 5}}{{qed|lemma}}
=== Lemma $6$ ===
{{:Cowen's Theorem/Lemma 6}}{{qed|lemma}}
=== Lemma $7$ ===
{{:Cowen's Theorem/Lemma 7}}{{qed|lemma}}
Recall:
:From Lemma $2$:
::$\O \in M$
:From Lemma $7$:
::$M$ is closed under $g$ relative to $x$
:From Lemma $4$:
::$M$ is closed under chain unions.
Hence by definition:
:$M$ is superinductive under $g$.
=== Lemma $8$ ===
{{:Cowen's Theorem/Lemma 8}}{{qed|lemma}}
We have {{apriori}} that $M$ is superinductive under $g$.
Let $A$ be superinductive under $g$.
Let $x \in M$.
Then:
:$x \in M_x$
and from Lemma $8$:
:$M_x \subseteq A$
Hence:
:$x \in A$
As $x$ is arbitrary, it follows by definition of subclass that:
:$M \subseteq A$.
Hence by definition $M$ is minimally superinductive under $g$.
{{qed}}
Theorem: Properties of Limit at Minus Infinity of Real Function/Sum Rule

Let $a \in \R$. 
Let $f, g : \hointl {-\infty} a \to \R$ be real functions such that: 
:$\ds \lim_{x \mathop \to -\infty} \map f x$ and $\ds \lim_{x \mathop \to -\infty} \map g x$ exist
where $\ds \lim_{x \mathop \to -\infty}$ denotes the limit at $-\infty$.
Then: 
:$\ds \lim_{x \mathop \to -\infty} \paren {\map f x + \map g x}$ exists
with: 
:$\ds \lim_{x \mathop \to -\infty} \paren {\map f x + \map g x} = \lim_{x \mathop \to \infty} \map f x + \lim_{x \mathop \to \infty} \map g x$

Proof:
From Properties of Limit at Minus Infinity of Real Function: Relation with Limit at Infinity, we have: 
:$\ds \lim_{x \mathop \to \infty} \map f {-x}$ and $\ds \lim_{x \mathop \to \infty} \map g {-x}$ exist.
From Properties of Limit at Infinity of Real Function: Sum Rule, we then have: 
:$\ds \lim_{x \mathop \to \infty} \paren {\map f {-x} + \map g {-x} }$ exists
with: 
:$\ds \lim_{x \mathop \to \infty} \paren {\map f {-x} + \map g {-x} } = \lim_{x \mathop \to \infty} \map f {-x} + \lim_{x \mathop \to \infty} \map g {-x}$
From Properties of Limit at Minus Infinity of Real Function: Relation with Limit at Infinity, this gives: 
:$\ds \lim_{x \mathop \to -\infty} \paren {\map f x + \map g x} = \lim_{x \mathop \to \infty} \map f x + \lim_{x \mathop \to \infty} \map g x$
{{qed}}
Category:Properties of Limit at Minus Infinity of Real Function
ptzv44yzc35kui8qhyusrzsl8m7bals
Theorem: Properties of Limit at Minus Infinity of Real Function/Product Rule

Let $a \in \R$. 
Let $f, g : \hointl {-\infty} a \to \R$ be real functions such that: 
:$\ds \lim_{x \mathop \to -\infty} \map f x$ and $\ds \lim_{x \mathop \to -\infty} \map g x$ exist
where $\ds \lim_{x \mathop \to -\infty}$ denotes the limit at $-\infty$.
Then: 
:$\ds \lim_{x \mathop \to -\infty} \paren {\map f x \map g x}$ exists
with: 
:$\ds \lim_{x \mathop \to -\infty} \paren {\map f x \map g x} = \paren {\lim_{x \mathop \to \infty} \map f x} \paren {\lim_{x \mathop \to \infty} \map g x}$

Proof:
From Properties of Limit at Minus Infinity of Real Function: Relation with Limit at Infinity, we have: 
:$\ds \lim_{x \mathop \to \infty} \map f {-x}$ and $\ds \lim_{x \mathop \to \infty} \map g {-x}$ exist.
From Properties of Limit at Infinity of Real Function: Product Rule, we then have: 
:$\ds \lim_{x \mathop \to \infty} \paren {\map f {-x} \map g {-x} }$ exists
with: 
:$\ds \lim_{x \mathop \to \infty} \paren {\map f {-x} \map g {-x} } = \paren {\lim_{x \mathop \to \infty} \map f {-x} } \paren {\lim_{x \mathop \to \infty} \map g {-x} }$
From Properties of Limit at Minus Infinity of Real Function: Relation with Limit at Infinity, this gives: 
:$\ds \lim_{x \mathop \to -\infty} \paren {\map f x \map g x} = \paren {\lim_{x \mathop \to \infty} \map f x} \paren {\lim_{x \mathop \to \infty} \map g x}$
{{qed}}
Category:Properties of Limit at Minus Infinity of Real Function
byxfptf8vs0vep2qpu0v61lxdqwa959
Theorem: Properties of Limit at Minus Infinity of Real Function/Multiple Rule

Let $a, \alpha \in \R$. 
Let $f : \hointl {-\infty} a \to \R$ be a real function such that: 
:$\ds \lim_{x \mathop \to -\infty} \map f x$ exists
where $\ds \lim_{x \mathop \to -\infty}$ denotes the limit at $-\infty$.
Then: 
:$\ds \lim_{x \mathop \to -\infty} \paren {\alpha \map f x}$ exists
with:
:$\ds \lim_{x \mathop \to -\infty} \paren {\alpha \map f x} = \alpha \lim_{x \mathop \to -\infty} \map f x$

Proof:
From Properties of Limit at Minus Infinity of Real Function: Relation with Limit at Infinity, we have: 
:$\ds \lim_{x \mathop \to \infty} \map f {-x}$ exists.
From Properties of Limit at Infinity of Real Function: Multiple Rule, we then have: 
:$\ds \lim_{x \mathop \to \infty} \paren {\alpha \map f {-x} }$ exists
with:
:$\ds \lim_{x \mathop \to \infty} \paren {\alpha \map f {-x} } = \alpha \lim_{x \mathop \to \infty} \map f {-x}$
From Properties of Limit at Minus Infinity of Real Function: Relation with Limit at Infinity, this gives: 
:$\ds \lim_{x \mathop \to -\infty} \paren {\alpha \map f x} = \alpha \lim_{x \mathop \to -\infty} \map f x$
{{qed}}
Category:Properties of Limit at Minus Infinity of Real Function
o8i91y69wwtwcsuje2vncctz74awgbf
Theorem: Properties of Limit at Minus Infinity of Real Function/Combined Sum Rule

Let $a, \alpha, \beta \in \R$. 
Let $f, g : \hointl {-\infty} a \to \R$ be real functions such that: 
:$\ds \lim_{x \mathop \to -\infty} \map f x$ and $\ds \lim_{x \mathop \to -\infty} \map g x$ exist
where $\ds \lim_{x \mathop \to -\infty}$ denotes the limit at $-\infty$.
Then: 
:$\ds \lim_{x \mathop \to -\infty} \paren {\alpha \map f x + \beta \map g x}$ exists
with: 
:$\ds \lim_{x \mathop \to -\infty} \paren {\alpha \map f x + \beta \map g x} = \alpha \lim_{x \mathop \to \infty} \map f x + \beta \lim_{x \mathop \to \infty} \map g x$

Proof:
From Properties of Limit at Minus Infinity of Real Function: Multiple Rule:
:$\ds \lim_{x \mathop \to -\infty} \paren {\alpha \map f x}$ exists
with:
:$\ds \lim_{x \mathop \to -\infty} \paren {\alpha \map f x} = \alpha \lim_{x \mathop \to -\infty} \map f x$
and:
:$\ds \lim_{x \mathop \to -\infty} \paren {\beta \map g x}$ exists
with:
:$\ds \lim_{x \mathop \to -\infty} \paren {\beta \map g x} = \beta \lim_{x \mathop \to -\infty} \map g x$
From Properties of Limit at Minus Infinity of Real Function: Sum Rule, we then have: 
:$\ds \lim_{x \mathop \to -\infty} \paren {\alpha \map f x + \beta \map g x}$ exists
with: 
{{begin-eqn}}
{{eqn	| l = \lim_{x \mathop \to -\infty} \paren {\alpha \map f x + \beta \map g x}
		| r = \lim_{x \mathop \to -\infty} \paren {\alpha \map f x} + \lim_{x \mathop \to -\infty} \paren {\beta \map g x}
}}
{{eqn	| r = \alpha \lim_{x \mathop \to -\infty} \map f x + \beta \lim_{x \mathop \to -\infty} \map g x
}}
{{end-eqn}}
{{qed}}
Category:Properties of Limit at Minus Infinity of Real Function
qacdp2x81bm9f72258k1e2n36lybi0t
Theorem: Properties of Limit at Minus Infinity of Real Function/Difference Rule

Let $a, \alpha, \beta \in \R$. 
Let $f, g : \hointl {-\infty} a \to \R$ be real functions such that: 
:$\ds \lim_{x \mathop \to -\infty} \map f x$ and $\ds \lim_{x \mathop \to -\infty} \map g x$ exist
where $\ds \lim_{x \mathop \to -\infty}$ denotes the limit at $-\infty$.
Then: 
:$\ds \lim_{x \mathop \to -\infty} \paren {\map f x - \map g x}$ exists
with: 
:$\ds \lim_{x \mathop \to -\infty} \paren {\map f x - \map g x} = \lim_{x \mathop \to \infty} \map f x - \lim_{x \mathop \to \infty} \map g x$

Proof:
This is the combined sum rule with $\alpha = 1$, $\beta = -1$.
{{qed}}
Category:Properties of Limit at Minus Infinity of Real Function
sh5s1iky4cueqryz6iv0ppoahoz2pje
Theorem: Limit of Constant Function/Two-Sided Limit at Real Number

Let $a, b \in \R$.
Define $f : \R \to \R$ by: 
:$\map f x = a$ for each $x \in \R$. 
Then: 
:$\ds \lim_{x \mathop \to b} \map f x = a$
where $\ds \lim_{x \mathop \to b}$ denotes the limit as $x \to b$.

Proof:
We have: 
:$\size {\map f x - a} = 0$ for all $x \in \R$. 
So for any $\epsilon > 0$ and $\delta > 0$, we have: 
:$\size {\map f x - a} < \epsilon$ for all $x \in \R$ with $\size {x - b} < \delta$.
So by the definition of the limit as $x \to b$, we have: 
:$\ds \lim_{x \mathop \to b} \map f x = a$
{{qed}}
Category:Limit of Constant Function
jq12833zearkbgqiak6pysigszls74k
Theorem: Limit of Constant Function/Limit at Infinity

Let $a, b \in \R$.
Define $f : \R \to \R$ by: 
:$\map f x = a$ for each $x \in \R$. 
Then: 
:$\ds \lim_{x \mathop \to \infty} \map f x = a$
where $\ds \lim_{x \mathop \to \infty}$ denotes the limit at $+\infty$.

Proof:
We have: 
:$\size {\map f x - a} = 0$ for all $x \in \R$. 
So for any $\epsilon > 0$ and $M \in \R$, we have:
:$\size {\map f x - a} < \epsilon$ for all $x \in \R$ with $x \ge M$.
So from the definition of the limit at $+\infty$, we have: 
:$\ds \lim_{x \mathop \to \infty} \map f x = a$
{{qed}}
Category:Limit of Constant Function
Category:Limit at Infinity
a0oiov9hnwhl0olku2uhi77m0zudolw
Theorem: Limit of Constant Function/Limit at Minus Infinity

Let $a, b \in \R$.
Define $f : \R \to \R$ by: 
:$\map f x = a$ for each $x \in \R$. 
Then: 
:$\ds \lim_{x \mathop \to -\infty} \map f x = a$
where $\ds \lim_{x \mathop \to -\infty}$ denotes the limit at $-\infty$.

Proof:
We have: 
:$\size {\map f x - a} = 0$ for all $x \in \R$. 
So for any $\epsilon > 0$ and $M \in \R$, we have:
:$\size {\map f x - a} < \epsilon$ for all $x \in \R$ with $x \le M$.
So from the definition of the limit at $-\infty$, we have: 
:$\ds \lim_{x \mathop \to -\infty} \map f x = a$
{{qed}}
Category:Limit of Constant Function
Category:Limit at Minus Infinity
s4wgcg6o6tyfeu5vkurcbl7i0ulsxf3
Theorem: Limit to Negative Infinity of Distribution Function of Finite Signed Borel Measure

Let $\mu$ be a finite signed Borel measure on $\R$.
Let $F_\mu$ be the distribution function of $\mu$. 
Then: 
:$\ds \lim_{x \mathop \to -\infty} \map {F_\mu} x = 0$
where $\ds \lim_{x \mathop \to -\infty}$ denotes the limit at $-\infty$.

Proof:
Let $\tuple {\mu^+, \mu^-}$ be the Jordan decomposition of $\mu$.
From Decomposition of Distribution Function of Finite Signed Borel Measure, we have: 
:$F_\mu = F_{\mu^+} - F_{\mu^-}$
where $F_{\mu^+}$ and $F_{\mu^-}$ are the distribution functions of $\mu^+$ and $\mu^-$ respectively.
From Limit of Distribution Function of Finite Borel Measure at Negative Infinity, we have: 
:$\ds \lim_{x \mathop \to -\infty} \map {F_{\mu^+} } x = 0$
and:
:$\ds \lim_{x \mathop \to -\infty} \map {F_{\mu^-} } x = 0$
From Properties of Limit at Minus Infinity of Real Function: Difference Rule, we have that: 
:$\ds \lim_{x \mathop \to -\infty} \paren {\map {F_{\mu^+} } x - \map {F_{\mu^-} } x} = 0 - 0 = 0$
So:
:$\ds \lim_{x \mathop \to -\infty} \map {F_\mu} x = 0$
{{qed}}
Theorem: Equivalence of Definitions of Primitive Root of Unity

Let $n \in \Z_{> 0}$ be a strictly positive integer.
Let $F$ be a field.
Let $U_n$ denote the set of all $n$-th roots of unity.
{{TFAE|def=Primitive Root of Unity}}
=== Definition 1 ===
{{:Definition:Primitive Root of Unity/Definition 1}}
=== Definition 2 ===
{{:Definition:Primitive Root of Unity/Definition 2}}

Proof:
=== Definition 1 implies Definition 2 ===
Let $\alpha \in U_n$ such that:
:$U_n = \set{1, \alpha, \alpha^2, \ldots, \alpha^{n-1}}$
By {{Defof|Power of Field Element}}:
:$\alpha = \alpha^1$
Hence:
:$U_n = \set{1, \alpha^1, \alpha^2, \ldots, \alpha^{n-1}}$
By {{Defof|Explicit Set Definition}}:
:$\forall m \in \N: 0 < m < n : \alpha^m \ne 1$ 
{{qed|lemma}}
Theorem: Measure of Half-Open Interval as Difference of Distribution Function

Let $a, b \in \R$. 
Let $\mu$ be a finite Borel measure on $\R$.
Let $F_\mu$ be the distribution function of $\mu$.
Then: 
:$\map \mu {\hointl a b} = \map {F_\mu} b - \map {F_\mu} a$

Proof:
Note that: 
:$\map \mu {\hointl {-\infty} a} < \infty$
since $\mu$ is finite.
Then, we have: 
{{begin-eqn}}
{{eqn	| l = \map {F_\mu} b - \map {F_\mu} a
		| r = \map \mu {\hointl {-\infty} b} - \map \mu {\hointl {-\infty} a}
}}
{{eqn	| r = \map \mu {\hointl {-\infty} b \setminus \hointl {-\infty} a}
		| c = Measure of Set Difference with Subset
}}
{{eqn	| r = \map \mu {\hointl a b}
		| c = Difference of Unbounded Closed Intervals
}}
{{end-eqn}}
{{qed}}