nyuuzyou/wikis huggingface dataset:
Expression for Set of Points at which Sequence of Functions does not Converge to Given Function

== Theorem ==
Let $X$ be a set. 
Let $f : X \to \R$ be a real function.
For each $n \in \N$, let $f_n : X \to \R$ be a real function.
Then we have: 
:$\ds \set {x \in X : \sequence {\map {f_n} x}_{n \in \N} \text { does not converge to } \map f x} = \bigcup_{k \mathop = 1}^\infty \bigcap_{N \mathop = 1}^\infty \bigcup_{n \mathop = N}^\infty \set {x \in X : \size {\map {f_n} x - \map f x} \ge \frac 1 k}$
 
== Proof ==
It helps to rewrite:
We have that $\sequence {\map {f_n} x}_{n \in \N}$ does not converge to $\map f x$ :
:there exists a real number $\epsilon > 0$ such that for each $N \in \N$ there exists $n \ge N$ such that $\size {\map {f_n} x - \map f x} \ge \epsilon$
Clearly then, setting $\epsilon = 1/k$, if $x \in X$ is such that: 
:there exists $k \in \N$ such that for each $N \in \N$ there exists $n \ge N$ such that $\size {\map {f_n} x - \map f x} \ge \dfrac 1 k$ 
we have that: 
:$\sequence {\map {f_n} x}_{n \in \N}$ does not converge.
So:
:$\ds \set {x \in X : \text {there exists some } k \in \N \text { such that for each } N \in \N \text { there exists } n \ge N \text { such that } \size {\map {f_n} x - \map f x} \ge \frac 1 k} \subseteq \set {x \in X : \sequence {\map {f_n} x}_{n \in \N} \text { does not converge to } \map f x}$
Now suppose that $x \in X$ is such that: 
:there exists a real number $\epsilon > 0$ such that for each $N \in \N$ there exists $n \ge N$ such that $\size {\map {f_n} x - \map f x} \ge \epsilon$
Pick $k \in \N$ sufficiently large so that: 
:$\epsilon \ge \dfrac 1 k$ 
Then we have that: 
:there exists $k \in \N$ such that for each $N \in \N$ there exists $n \ge N$ such that $\size {\map {f_n} x - \map f x} \ge \dfrac 1 k$.
So:
:$\ds \set {x \in X : \sequence {\map {f_n} x}_{n \in \N} \text { does not converge to } \map f x} \subseteq \set {x \in X : \text {there exists some } k \in \N \text { such that for each } N \in \N \text { there exists } n \ge N \text { such that } \size {\map {f_n} x - \map f x} \ge \frac 1 k}$
Then from the definition of set equality:
:$\ds \set {x \in X : \sequence {\map {f_n} x}_{n \in \N} \text { does not converge to } \map f x} = \set {x \in X : \text {there exists some } k \in \N \text { such that for each } N \in \N \text { there exists } n \ge N \text { such that } \size {\map {f_n} x - \map f x} \ge \frac 1 k}$
That is:
:$\ds \set {x \in X : \sequence {\map {f_n} x}_{n \in \N} \text { does not converge to } \map f x} = \bigcup_{k \mathop = 1}^\infty \bigcap_{N \mathop = 1}^\infty \bigcup_{n \mathop = N}^\infty \set {x \in X : \size {\map {f_n} x - \map f x} \ge \frac 1 k}$
Category:Convergence
Expression for bilinear function

== Theorem ==
Let $f$ be a real function of two independent variables, $f \in \R \times \R \to \R$.
Then:
:$\map f {x, y}$ is a linear function of $x$ when $y$ is equal to a real constant
:$\map f {x, y}$ is a linear function of $y$ when $x$ is equal to a real constant
 $f$ has the form:
:$\exists a, b, c, d \in \R: \forall {x, y} \in \R: \map f {x, y} = a x y + b x + c y + d$
== Proof ==
=== Sufficient Condition ===
Let:
:$\map f {x, y}$ be a linear function of $x$ when $y$ is equal to a real constant
:$\map f {x, y}$ be a linear function of $y$ when $x$ is equal to a real constant
We need to show that:
:$\exists a, b, c, d \in \R: \forall {x, y} \in \R: \map f {x, y} = a x y + b x + c y + d$
==== Expressions for $\map f {x, y}$ when either $x$ or $y$ is constant ====
We have:
:$\map f {x, y}$ is a linear function of $x$ when $y$ is equal to a real constant.
This means that:
:$\exists \alpha, \beta, y \in \R: \forall x \in \R: \map f {x, y} = \alpha x + \beta$
The real constants $\alpha$ and $\beta$ may depend on $y$ as $y$ is constant.
In other words:
:$\forall {x, y} \in \R: \map f {x, y} = \map {a_1} y x + \map {a_2} y$
where $a_1$ and $a_2$ are real functions, $a_1, a_2 \in \R \to \R$.
By symmetry, we find from:
:$\map f {x, y}$ is a linear function of $y$ when $x$ is equal to a real constant
that:
:$\forall {x, y} \in \R: \map f {x, y} = \map {b_1} x y + \map {b_2} x$
where $b_1$ and $b_2$ are real functions, $b_1, b2 \in \R \to \R$.
==== Expression for $\map f {x, y}$ for every value of $x$ and $y$ ====
We have:
In other words, $b_2$ is a linear function of $x$.
We have:
In other words, $b_1$ is a linear function of $x$.
In conclusion, we have:
This expression for $\map f {x, y}$ is of the sought for form:
:$\exists {a, b, c, d} \in \R: \forall {x, y} \in \R: \map f {x, y} = a x y + b x + c y + d$
=== Necessary Condition ===
Let:
:$\exists {a, b, c, d} \in \R: \forall {x, y} \in \R: \map f {x, y} = a x y + b x + c y + d$
We need to show that:
:$\map f {x, y}$ is a linear function of $x$ when $y$ is equal to a real constant
:$\map f {x, y}$ is a linear function of $y$ when $x$ is equal to a real constant
Let:
:$y$ be equal to a real constant.
We have:
So, $\map f {x, y}$ is a linear function of $x$ as $a y + b$ and $c y + d$ are constant.
Now, let:
:$x$ be equal to a real constant.
We have:
So, $\map f {x, y}$ is a linear function of $y$ as $a x + c$ and $b x + d$ are constant.
Hence the result.
Category:Linear Real Functions
Expression of Vector as Linear Combination from Basis is Unique

== Theorem ==
Let $V$ be a vector space of dimension $n$.
Let $\BB = \set {\mathbf x_1, \mathbf x_2, \ldots, \mathbf x_n}$ be a basis for $V$.
Let $\mathbf x \in V$ be any vector of $V$.
Then $\mathbf x$ can be expressed as a unique linear combination of elements of $\BB$.
=== General Result ===
== Proof ==
=== Proof of Existence ===
By the definition of basis, $\BB$ is a spanning set.
Hence the result, by the definition of a spanning set.
=== Proof of Uniqueness ===
 otherwise, that:
:$\ds \sum_{k \mathop = 1}^n \alpha_k \mathbf x_k = \mathbf x = \sum_{k \mathop = 1}^n \beta_k \mathbf x_k$
where $\alpha_i \ne \beta_i$ for some $1 \le i \le n$.
Then:
However, we have that $\BB = \set {\mathbf x_1, \mathbf x_2, \ldots, \mathbf x_n}$ is a basis for $V$.
So, by definition, $\BB$ is a linearly independent set.
This means that, for $1 \le i \le n$:
:$\alpha_i - \beta_i = 0$
and hence $\alpha_i = \beta_i$ for all $1 \le i \le n$.
This contradicts our assumption that $\alpha_i \ne \beta_i$ for some $i$.
Hence the result, from Proof by Contradiction.
== Also see ==
* Definition:Coordinate Vector
== Sources ==
* : Chapter $\text I$: Vector Algebra: $\S 1$.
* : Chapter $\text {I}$: Elementary Definitions: $\S 4$. Vector Spaces
* : Chapter $7$: Vector Spaces: $\S 35$. Coordinates
* 
* 
* 
Category:Linear Algebra
Category:Bases of Vector Spaces
Expression of Vector as Linear Combination from Basis is Unique/General Result

== Theorem ==
Let $V$ be a vector space over a division ring $R$.
Let $B$ be a basis for $V$.
Let $x \in V$.
Then there is a unique finite subset $C$ of $R \times B$ such that:
:$\ds x = \sum_{\tuple {r, v} \mathop \in C} r \cdot v$
:$\forall \tuple {r, v} \in C: r \ne 0_R$
== Proof ==
=== Existence ===
The existence of $C$ follows immediately from the definition of a basis.
=== Uniqueness ===
Let $C, D$ be finite subsets of $R \times B$ satisfying the requirements.
Let $Q = \set {v: \exists r \in R: \tuple {r, v} \in C \cup D}$.
Let $V' = \map \span Q$.
Then $V'$ is a finite-dimensional vector space with basis $Q$ and $x \in V'$.
Thus the theorem follows from Expression of Vector as Linear Combination from Basis is Unique.
Category:Vector Spaces
Category:Linear Algebra
Exradius of Triangle in Terms of Circumradius

== Theorem ==
Let $\triangle ABC$ be a triangle whose sides are $a$, $b$ and $c$ opposite vertices $A$, $B$ and $C$ respectively.
Let $\rho_a$ be the exradius of $\triangle ABC$ $a$.
Let $R$ be the circumradius of $\triangle ABC$.
Then:
:$\rho_a = 4 R \sin \dfrac A 2 \cos \dfrac B 2 \cos \dfrac C 2$
== Proof 1 ==
== Proof 2 ==
== Sources ==
* : $\text V$. Trigonometry: Formulae $(56)$
Category:Exradius of Triangle in Terms of Circumradius
Category:Circumcircles of Triangles
Category:Excircles of Triangles
Extend Theory to Satisfy Witness Property/Lemma

== Lemma ==
Let $\LL$ be a language of predicate logic.
Let $\FF$ be a set of $\LL$-sentences.
Suppose that, for every $\LL$-WFF $\phi$ of $1$ free variable $x$:
:There exists some term $t_\phi$ containing no variables such that:
::$\paren {\exists x : \map \phi x} \implies \map \phi {x := t_\phi}$
:is an element of $\FF$.
Then $\FF$ satisfies the witness property.
== Proof ==
Let $\phi \in \FF$ be an arbitrary $\LL$-WFF of $1$ free variable $x$.
Suppose that $\FF \models_{\mathrm{PL}} \exists x : \map \phi x$.
Then, every $\LL$-structure $\MM$ satisfies:
:$\map {\operatorname{val}_\MM} {\exists x : \map \phi x} = \top$
Additionally, by the assumption on $\FF$:
:$\map {\operatorname{val}_\MM} {\paren {\exists x : \map \phi x} \implies \map \phi {x := t_\phi}} = \top$
By examining the truth function of conditional, we can conclude that:
:$\map {\operatorname{val}_\MM} {\map \phi {x := t_\phi}} = \top$
As this holds for every $\MM$, we conclude that:
:$\FF \models_{\mathrm{PL}} \map \phi {x := t_\phi}$
As $\phi$ was arbitrary, the witness property holds.
Category:Model Theory for Predicate Logic
Extendability Theorem for Function Continuous on Open Interval

== Theorem ==
Let $f$ be a continuous real function that is defined on an open interval $\openint a b$.
Let $g$ be a real function that satisfies:
:$g$ is defined on $\closedint a b$
:$g$ is continuous on $\closedint a b$
:$g = f$ on $\openint a b$.
Then $g$ exists $\ds \lim_{x \mathop \to a^+} \map f x$ and $\ds \lim_{x \mathop \to b^-} \map f x$ exist.
== Proof ==
=== Necessary Condition ===
Assume that $g$ exists.
We need to prove that the limits $\ds \lim_{x \mathop \to a^+} \map f x$ and $\ds \lim_{x \mathop \to b^-} \map f x$ exist.
$g$ is continuous at the end points $a$ and $b$ of its domain as $g$ is continuous on $\closedint a b$.
$g$ is right-continuous at $a$ and left-continuous at $b$.
This means that $\map g a = \ds \lim_{x \mathop \to a^+} \map g x$ and $\map g b = \ds \lim_{x \mathop \to b^-} \map g x$.
In turn, this means that the expressions $\ds \lim_{x \mathop \to a^+} \map g x$ and $\ds \lim_{x \mathop \to b^-} \map g x$ exist.
The two $x$ parameters as being part of the two limiting processes in these expressions can be considered confined to $\openint a b$.
Therefore, $g$ in these two expressions can be replaced by $f$ as $g = f$ on $\openint a b$.
We conclude that $\ds \lim_{x \mathop \to a^+} \map f x$ and $\ds \lim_{x \mathop \to b^-} \map f x$ exist.
=== Sufficient Condition ===
Let $\ds \lim_{x \mathop \to a^+} \map f x$ and $\ds \lim_{x \mathop \to b^-} \map f x$ exist.
We need to prove that a function $g$ with the properties listed in the theorem exists.
Define $g = f$ on $\openint a b$.
Define:
:$\map g a = \ds \lim_{x \mathop \to a^+} \map f x$
:$\map g b = \ds \lim_{x \mathop \to b^-} \map f x$
$g$ is defined at $a$ and $b$ as ensured by the existence of the limits on the right hand sides of these two equations.
We know that $f$ is continuous on $\openint a b$.
Therefore, $g$ too is continuous on $\openint a b$ as $g = f$ there.
It remains to show that $g$ is continuous at $a$ and $b$.
$\map g a = \ds \lim_{x \mathop \to a^+} \map f x$ per definition.
$x$ can be considered as being an element of $\openint a b$ as the limiting process at $a$ requires $x$ to approach $a$ from above.
$\map g b = \ds \lim_{x \mathop \to b^-} \map f x$ per definition.
$x$ can be considered as being an element of $\openint a b$ as the limiting process at $b$ requires $x$ to approach $b$ from below.
Therefore, the two equations above can be written:
:$\map g a = \ds \lim_{x \mathop \to a^+} \map g x$
:$\map g b = \ds \lim_{x \mathop \to b^-} \map g x$
as $g = f$ on $\openint a b$.
We conclude that $g$ is continuous at $a$ and $b$ as these two equations are exactly the definitions of continuity for $g$ at respectively $a$ and $b$.
== Also see ==
* Extendability Theorem for Derivatives Continuous on Open Intervals
Category:Continuous Real Functions
Extendability Theorem for Intersection Numbers

== Theorem ==
Let $X = \partial W$ be a smooth manifold which is the boundary of a smooth compact manifold $W$.
Let:
:$Y$ be a smooth manifold
:$Z$ be a closed smooth submanifold of $Y$
:$f: X \to Y$ be a smooth map.
Let there exist a smooth map $g: W \to Y$ such that $g \restriction_X = f$.
Then:
:$\map I {f, Z} = 0$
where $\map I {f, Z}$ is the intersection number.
=== Corollary ===
== Proof ==
Category:Manifolds
Extendability Theorem for Intersection Numbers/Corollary

== Corollary to Extendability Theorem for Intersection Numbers ==
Let $f: X \to Y$ be a smooth map of compact oriented manifolds having the same dimension.
Let $X = \partial W$, where $W$ is compact.
If there is a smooth map $g: W \to Y$ such that $g {\restriction_X} = f$, then:
:$\map \deg f = 0$
where $\map \deg f$ denotes the degree of $f$.
== Proof ==
Follows immediately from the Extendability Theorem for Intersection Numbers.
Category:Topology
Extended Completeness Theorem for Propositional Tableaux and Boolean Interpretations

== Theorem ==
Tableau proofs (in terms of propositional tableaux) are a strongly complete proof system for boolean interpretations.
More precisely, for every countable collection $\mathbf H$ of WFFs of propositional logic and every WFF $\mathbf A$:
:$\mathbf H \models_{\mathrm{BI} } \mathbf A$ implies $\mathbf H \vdash_{\mathrm{PT} } \mathbf A$
== Proof ==
Let $\mathbf A$ be a semantic consequence of $\mathbf H$ for boolean interpretations.
That is, if $v \models_{\mathrm{BI} } \mathbf H$, also $v \models_{\mathrm{BI} } \mathbf A$.
By the truth function for $\neg$, it follows that for such $v$:
:$v \not\models_{\mathrm{BI}} \neg \mathbf A$
Therefore, $\mathbf H' := \mathbf H \cup \set {\mathbf A}$ is unsatisfiable for boolean interpretations.
Since $\mathbf H'$ is countable, it follows from the Compactness Theorem for Boolean Interpretations that:
:Some finite $\mathbf H' ' \subseteq \mathbf H'$ is unsatisfiable.
By the Tableau Extension Lemma, there exists a finite finished tableau $T$ for $\mathbf H$.
By definition of finished tableau, every branch of $T$ is finished or contradictory.
From the Corollary to the Finished Branch Lemma, $\Phi \sqbrk \Gamma$ is satisfiable for any finished branch $\Gamma$.
But since $\mathbf H' ' \subseteq \Phi \sqbrk \Gamma$, this would imply $\mathbf H' '$ is also satisfiable, which is a contradiction.
It follows that every branch of $T$ is contradictory.
Since $\mathbf H' ' \subseteq \mathbf H'$, replacing the hypothesis set $\mathbf H'$ of $T$ with $\mathbf H' '$ yields another propositional tableau $T'$.
Since every branch of $T'$ is contradictory, $T'$ is a tableau confutation of $\mathbf H'$.
Recalling that $\mathbf H' = \mathbf H \cup \set {\neg \mathbf A}$, we conclude that $T'$ is a tableau proof of $\mathbf A$ from $\mathbf H$:
:$\mathbf H \vdash_{\mathrm{PT} } \mathbf A$
== Also see ==
The Extended Soundness Theorem for Propositional Tableaux and Boolean Interpretations in which is proved:
:If $\mathbf H \vdash \mathbf A$, then $\mathbf H \models \mathbf A$.
== Sources ==
* : $\S 1.10$: Completeness: Theorem $1.10.3$
Category:Completeness Theorem
Category:Boolean Interpretations
Category:Propositional Tableaux
Category:Named Theorems
Extended Euclidean Algorithm

== Algorithm ==
The extended Euclidean algorithm is a method for:
: finding the greatest common divisor (GCD) $d$ of two strictly positive integers $m$ and $n$
: computing two integers $a$ and $b$ such that $a m + b n = d$.
Let $m, n \in \Z_{>0}$.
:$\mathbf 1:$ Initialise.
::Set $a' \gets b \gets 1, a \gets b\,' \gets 0, c \gets m, d \gets n$.
:$\mathbf 2:$ Divide.
::Let $q$ and $r$ be the quotient and remainder respectively of $ c / d$.
::(Thus we have $c = q d + r$ such that $0 \le r < d$.)
:$\mathbf 3:$ Remainder zero?
::If $r = 0$, the algorithm terminates.
::(Thus we have $a m + b n = d$ as required.)
:$\mathbf 4:$ Recycle.
::Set $c \gets d, d \gets r, t \gets a', a' \gets a, a \gets t - q a, t \gets b\,', b\,' \gets b, b \gets t - q b$, then go to Step $\mathbf 2$.
== Proof ==
Thus the GCD of $m$ and $n$ is the value of the variable $d$ at the end of the algorithm.
== Sources ==
* : $\S 1.2.1$: Mathematical Induction
Category:Euclidean Algorithm
Extended Mean Value Theorem

== Theorem ==
Let $f$ be a real function which is continuous on the closed interval $\closedint a b$ and differentiable on the open interval $\openint a b$.
Let $f'$ be the derivative of $f$.
Let $f'$ also be a real function which is continuous on the closed interval $\closedint a b$ and differentiable on the open interval $\openint a b$.
Then:
:$\exists \xi \in \openint a b: \map f b = \map f a + \paren {b - a} \map {f'} a + \dfrac 1 {2!} \paren {b - a}^2 \map {f' '} \xi$
== Proof ==
== Also known as ==
== Also see ==
* Mean Value Theorem
== Sources ==
* 
* 
Category:Extended Mean Value Theorem
Category:Mean Value Theorem
Category:Differential Calculus
Category:Named Theorems
Extended Real Addition is Associative

== Theorem ==
Extended real addition $+_{\overline{\R}}$ is commutative.
That is, for all $x, y, z \in \overline \R$:
:$(1): \quad x +_{\overline \R} \paren {y +_{\overline \R} z} = \paren {x +_{\overline \R} y} +_{\overline \R} z$
whenever at least one of the sides is defined.
== Proof ==
When $x, y, z \in \R$, then $(1)$ follows from Real Addition is Associative.
From the definition of $+_{\overline \R}$, it follows that either expression in $(1)$ is defined at most one of $+\infty$ and $-\infty$ occurs.
The case where neither occurs is already covered above; now assume that $+\infty$ occurs (the case with $-\infty$ is similar).
By Extended Real Addition is Commutative, it suffices to consider the cases $x = +\infty$ and $y = +\infty$.
Suppose $x = +\infty$.
Then as $y \ne -\infty$ and $z \ne -\infty$, it follows that $\paren {+\infty} +_{\overline \R} y = +\infty$, and $\paren {+\infty} +_{\overline \R} z = +\infty$.
Hence the in $(1)$ equals $+\infty$.
But $y +_{\overline \R} z \ne -\infty$ as well, and so the also equals $+\infty$.
Now suppose $y = +\infty$.
Then, again, $x +_{\overline \R} \paren {+\infty} = +\infty$ and $\paren {+\infty} +_{\overline \R} z = +\infty$.
The result follows by applying these two equalities in the appropriate order on both the and the of $(1)$.
Hence the result, from Proof by Cases.
Category:Extended Real Numbers
Extended Real Addition is Commutative

== Theorem ==
Extended real addition $+_{\overline{\R}}$ is commutative.
That is, for all $x, y \in \overline{\R}$:
:$x +_{\overline{\R}} y = y +_{\overline{\R}} x$
whenever at least one of the sides is defined.
== Proof ==
When $x,y \in \R$, then $x +_{\overline{\R}} y = y +_{\overline{\R}} x$ follows from Real Addition is Commutative.
The remaining cases where the expressions are defined, are already imposed in the definition of $+_{\overline{\R}}$.
Category:Extended Real Numbers
Extended Real Multiplication is Associative

== Theorem ==
Extended real multiplication $\cdot_{\overline \R}$ is commutative.
That is, for all $x, y, z \in \overline \R$:
:$(1): \quad x \cdot_{\overline \R} \left({y \cdot_{\overline \R} z}\right) = \left({x \cdot_{\overline \R} y}\right) \cdot_{\overline \R} z$
== Proof ==
When $x, y, z \in \R$, then $(1)$ follows from Real Multiplication is Associative.
Next, the cases where at least one of $+\infty$ and $-\infty$ occurs need to be dealt with.
Category:Extended Real Numbers
Extended Real Multiplication is Commutative

== Theorem ==
Extended real multiplication $\times_{\overline \R}$ is commutative.
That is, for all $x, y \in \overline \R$:
:$x \times_{\overline \R} y = y \times_{\overline \R} x$
== Proof ==
Let $x, y \in \R$.
Then from Real Multiplication is Commutative:
:$x \times_{\overline \R} y = y \times_{\overline \R} x$
The remaining cases are explicitly imposed in the definition of $\times_{\overline \R}$.
Category:Extended Real Numbers
Extended Real Numbers under Multiplication form Commutative Monoid

== Theorem ==
Denote with $\overline \R$ the extended real numbers.
Denote with $\cdot_{\overline \R}$ the extended real multiplication.
The algebraic structure $\struct {\overline \R, \cdot_{\overline \R} }$ is a commutative monoid.
== Proof ==
By Extended Real Numbers under Multiplication form Monoid, $\struct {\overline \R, \cdot_{\overline \R} }$ is a monoid.
By Extended Real Multiplication is Commutative, $\cdot_{\overline \R}$ is commutative.
Hence $\struct {\overline \R, \cdot_{\overline \R} }$ is a commutative monoid.
Category:Extended Real Numbers
Category:Examples of Commutative Monoids
Extended Real Numbers under Multiplication form Monoid

== Theorem ==
Denote with $\overline \R$ the extended real numbers.
Denote with $\cdot_{\overline \R}$ the extended real multiplication.
The algebraic structure $\struct {\overline \R, \cdot_{\overline \R} }$ is a monoid.
== Proof ==
Checking the axioms for a monoid in turn:
=== Closure ===
Immediate as $\cdot_{\overline \R}: \overline \R \times \overline \R \to \overline \R$ is a mapping.
=== Associativity ===
Proved on Extended Real Multiplication is Associative.
=== Identity ===
For all $x \in \R$, it holds that $1 \cdot_{\overline \R} x = x \cdot_{\overline \R} 1 = x$ by definition of $\cdot_{\overline \R}$ on $\R$.
Furthermore, by definition, $1 \cdot_{\overline \R} \paren {+\infty} = \paren {+\infty} \cdot_{\overline \R} 1 = \paren {+\infty}$.
Lastly $1 \cdot_{\overline \R} \paren {-\infty} = \paren {-\infty} \cdot_{\overline \R} 1 = \paren {-\infty}$.
That is, $1 \in \overline \R$ is an identity for $\cdot_{\overline \R}$.
Hence, satisfying all the axioms, $\struct {\overline \R, \cdot_{\overline \R} }$ is a monoid.
Category:Extended Real Numbers
Category:Examples of Monoids
Extended Real Sigma-Algebra Induces Borel Sigma-Algebra on Reals

== Theorem ==
Let $\overline \BB$ be the extended real $\sigma$-algebra.
Let $\map \BB \R$ be the Borel $\sigma$-algebra on $\R$.
Then:
:$\overline \BB_\R = \map \BB \R$
where $\overline \BB_\R$ denotes a trace $\sigma$-algebra.
== Proof ==
We have Euclidean Space is Subspace of Extended Real Number Space.
The result follows from Borel Sigma-Algebra of Subset is Trace Sigma-Algebra.
== Sources ==
* : $8.2$
* : $\S 8$: Problem $2$
Category:Extended Real Numbers
Category:Sigma-Algebras
Extended Rolle's Theorem

== Theorem ==
Let $f: D \to \R$ be differentiable on a closed interval $I \subseteq \R$.
Let $x_0 < x_1 < \dots < x_n \in I$.
Let $\map f {x_i} = 0$ for $i = 0, \ldots, n$.
Then for all $i = 0, \ldots, n-1$:
:$\exists \xi_i \in \openint {x_i} {x_{i + 1} }: \map {f'} {\xi_i} = 0$
== Proof ==
Since $f$ is differentiable on $I$, f is differentiable on $\closedint {x_i} {x_{i + 1} }$ for $i = 0, \ldots, n - 1$.
Thus a fortiori, $f$ is also continuous on the closed interval $\closedint {x_i} {x_{i + 1} }$ and differentiable on the open interval $\openint {x_i} {x_{i + 1} }$.
For $i = 0, \ldots, n$ we have $\map f {x_i} = 0$.
Hence the conditions of Rolle's Theorem are fulfilled on each interval which yields the result.
== Comment ==
If $f$ is differentiable multiple times, this theorem can be applied multiple times recursively until one runs out of zeroes, each interval pair $\openint {x_i} {x_{i + 1} }$, $\openint {x_{i + 1} } {x_{i + 2} }$ becoming $\openint {\xi_i} {\xi_{i + 1} }$ with $\map f {\xi_i} = 0$, $\map f {\xi_{i + 1} } = 0$ and all $\xi \in I$.
== Also see ==
* Rolle's Theorem
Category:Differentiable Real Functions
Category:Continuous Real Functions
Category:Rolle's Theorem