nyuuzyou/wikis huggingface dataset:
Raw Moment of Weibull Distribution

== Theorem ==
Let $X$ be a continuous random variable with the Weibull distribution with $\alpha, \beta \in \R_{> 0}$.
Let $n$ be a strictly positive integer. 
Then the $n$th raw moment $\expect {X^n}$ of $X$ is given by: 
:$\expect {X^n} = \beta^n \map \Gamma {1 + \dfrac n \alpha}$
where $\Gamma$ is the Gamma function.
== Proof == 
From the definition of the Weibull distribution, $X$ has probability density function:
:$\map {f_X} x = \alpha \beta^{-\alpha} x^{\alpha - 1} e^{-\paren {\frac x \beta}^\alpha}$
where $\Img X = \R_{\ge 0}$.
From the definition of the expected value of a continuous random variable: 
:$\ds \expect {X^n} = \int_0^\infty x^n \map {f_X} x \rd x$
Therefore:
Let: 
:$u = \paren {\dfrac x \beta}^\alpha$
Then by Chain Rule for Derivatives, we have:
:$\dfrac {\d u} {\d x} = \alpha \paren {\dfrac x \beta}^{\alpha - 1} \dfrac 1 \beta$
and also:
:$\paren {\beta u^{\frac 1 \alpha} }^n = x^n$
We can see that:
:$u \to 0$ as $x \to 0$
and
:$u \to \infty$ as $x \to \infty$
Plugging these results back into our integral above, we have:
Category:Weibull Distribution
Category:Raw Moments
Ray from Bounded Set Meets Boundary

== Theorem ==
Let $A \subseteq \R^n$ be a bounded subspace of real Euclidean $n$-space.
Let $\bsx_0 \in A$ be point of $A$.
Then, for every $\bsy \in \R^n \setminus \set \bszero$, there is some $t \in \R_{\ge 0}$ such that:
:$\bsx_0 + t \bsy \in \partial A$
where $\partial A$ denotes the boundary of $A$.
== Proof ==
For every $t \in \R$, let:
:$\map \bsx t = \bsx_0 + t \bsy$
Define:
:$D = \set {t \in \R_{\ge 0} : \map \bsx t \in A}$
As $\map \bsx 0 = \bsx_0 \in A$:
:$0 \in D$
so:
:$D$ is non-empty
By definition of bounded, there exists some $K \in \R$ such that:
:$\forall \bsx \in A: \size {\bsx - \bsx_0} \le K$
Suppose for arbitrary $t \in \R_{\ge 0}$ that $\map \bsx t \in A$.
Then:
Therefore, $D$ is bounded above.
By the Least Upper Bound Property, let:
:$t_D = \sup D$
We will show that:
:$\map \bsx {t_D} \in \partial A$
Let $N \subseteq \R^n$ be a neighborhood of $\map \bsx {t_D}$.
By definition, there exists some $\delta > 0$ such that:
:$\map {B_\delta} {\map \bsx {t_D}} \subseteq N$
We want to prove that:
:$A \cap \map {B_\delta} {\map \bsx {t_D}} \ne \O$
:$\overline A \cap \map {B_\delta} {\map \bsx {t_D}} \ne \O$
By Characterizing Property of Supremum of Subset of Real Numbers, there exists some $t_\delta \in D$ such that:
:$t_D - \dfrac \delta {\norm \bsy} < t_\delta \le t_D$
By definition of $D$:
:$\map \bsx {t_\delta} \in A$
Also:
Therefore:
:$\map \bsx {t_\delta} \in \map {B_\delta} {\map \bsx {t_D}}$
It immediately follows that:
:$A \cap \map {B_\delta} {\map \bsx {t_D}} \ne \O$
Now, let:
:$t'_\delta = t_D + \dfrac \delta {2 \norm \bsy}$
By definition of supremum, $t_D$ is an upper bound for $D$.
Therefore, since:
:$t'_\delta > t_D$
it follows that:
:$t'_\delta \notin D$
That is:
:$\map \bsx {t'_\delta} \notin A$
or:
:$\map \bsx {t'_\delta} \in \overline A$
Finally:
That is:
:$\map \bsx {t'_\delta} \in \map {B_\delta} {\map \bsx {t_D}}$
From the above, we have:
:$\map \bsx {t'_\delta} \in \overline A \cap \map {B_\delta} {\map \bsx {t_D}}$
That is:
:$\overline A \cap \map {B_\delta} {\map \bsx {t_D}} \ne \O$
From:
:$A \cap \map {B_\delta} {\map \bsx {t_D}} \ne \O$
:$\overline A \cap \map {B_\delta} {\map \bsx {t_D}} \ne \O$
we have proven that:
:$\map \bsx {t_D} \in \partial A$
by definition of boundary.
Therefore:
:$\bsx_0 + t_D \bsy \in \partial A$
Category:Bounded Metric Spaces
Ray from Interior of Compact Convex Set Meets Boundary Exactly Once

== Theorem ==
Let $A \subseteq \R^n$ be a compact convex subspace of real Euclidean $n$-space.
Let $\bsx_0 \in A^\circ$ be an interior point of $A$.
Then, for every $\bsy \in \R^n \setminus \bszero$, there is a unique $t \in \R_{> 0}$ such that:
:$\bsx_0 + t \bsy \in \partial A$
== Proof ==
By Compact Subspace of Metric Space is Bounded:
:$A$ is bounded
Then, by Ray from Bounded Set Meets Boundary, there is some $t \in \R_{\ge 0}$ such that:
:$\bsx_0 + t \bsy \in \partial A$
But, if $t = 0$, then:
:$\bsx_0 \in \partial A$
contradicting the definition of boundary, since $\bsx_0 \in A^\circ$.
Thus, $t > 0$.
Now, suppose that $t' \in \R_{> 0}$ also satisfies:
:$\bsx_0 + t' \bsy \in \partial A$
, suppose $t' \le t$.
By definition of interior point, there is some $\epsilon > 0$ such that:
:$\map {B_\epsilon} {\bsx_0} \subseteq A$
Let $\epsilon' = \dfrac {t - t'} t \epsilon$.
 $t' < t$.
Then, $\epsilon' > 0$.
Let $\bsx' \in \map {B_{\epsilon'}} {\bsx_0 + t' \bsy}$ be arbitrary.
Define:
:$\bsx = \bsx_0 + \dfrac t {t - t'} \paren {\bsx' - \paren {\bsx_0 + t' \bsy}}$
We have:
Therefore:
:$\bsx \in \map {B_\epsilon} {\bsx_0} \subseteq A$
Finally:
As $0 < t' < t$, it follows that:
:$0 < \dfrac {t'} t < 1$
Additionally, by Compact Subspace of Hausdorff Space is Closed:
:$\partial A \subseteq A$
Therefore:
:$\bsx_0 + t \bsy \in A$
So, by definition of convex:
:$\bsx' \in A$
As $\bsx' \in \map {B_{\epsilon'}} {\bsx_0 + t' \bsy}$ was arbitrary, it follows that:
:$\map {B_{\epsilon'}} {\bsx_0 + t' \bsy} \subseteq A$
Therefore, by definition:
:$\bsx_0 + t' \bsy \in A^\circ$
But we assumed that:
:$\bsx_0 + t' \bsy \in \partial A$
which is a contradiction.
Therefore, by Proof by Contradiction:
:$t' = t$
Category:Convex Sets (Vector Spaces)
Ray is Convex

== Theorem ==
Let $\struct {S, \preceq}$ be an ordered set.
Let $I$ be a ray, either open or closed.
Then $I$ is convex in $S$.
== Proof ==
The cases for upward-pointing and downward-pointing rays are equivalent.
, suppose that $U$ is an upward-pointing ray.
By the definition of a ray, there exists an $a \in S$ such that:
:$I = a^\succ$
or;
:$I = a^\succeq$
according to whether $U$ is open or closed.
Let $x, y, z \in S$ such that $x \prec y \prec z$ and $x, z \in I$.
Then:
:$a \preceq x \prec y$
so:
:$a \prec y$
Therefore:
:$y \in a^\succ \subseteq I$
Thus $I$ is convex.
== Also see ==
* Upper and Lower Closures are Convex
Category:Convex Sets (Order Theory)
Category:Rays (Order Theory)
Re-entrant Queen's Tour

== Theorem ==
Consider a chessboard $\CC$ of size $n \times n$ such that $n > 3$.
Then there exists a re-entrant queen's tour on $\CC$ of $2 n - 2$ moves.
For $n < 6$ it is necessary for the queen to move outside the boundary of the chessboard in order for this to happen.
== Proof ==
First it is shown that at least $2 n - 2$ moves are needed.
Let there be $R$ rows and $S$ columns which have none of the given moves on them.
The $R \times S$-square segment of this chessboard has a $2 R + 2 S - 4$ squares on its edge if $R$ and $S$ are both greater than $1$.
Each diagonal moves covers at most $2$ of these boundary square.
Thus in the set of moves there are at least:
:$R + S - 2$ diagonal moves
:$n - R$ horizontal moves
:$n - S$ vertical moves.
Thus there are at least $2 n - 2$ moves needed to cover the entire chessboard.
It remains to demonstrate that no more than $2 n - 2$ moves are needed.
== Historical Note ==
== Sources ==
* 
* : Answers: $416$. Sinking the Fishing-Boats
Category:Queen's Tours
Real-Valued Continuous Function Vanishing at Zero applied to Hermitian Element of Closed Ideal of Unital C*-Algebra is contained in Ideal

== Theorem ==
Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a unital $\text C^\ast$-algebra.
Let $I$ be a closed ideal.
Let $x \in I$ be Hermitian.
Let $\map {\sigma_A} x \subseteq \R$ be the spectrum of $x$ in $A$.
Let $K$ be a compact set such that $0 \in K$ and $\map {\sigma_A} x \subseteq K$. 
Let $f : K \to \R$ be a continuous function with $\map f 0 = 0$.
Let $\map f x$ be obtained from the continuous functional calculus, restricting $f$ to $\map {\sigma_A} x$.
Then $\map f x \in I$. 
=== Corollary ===
== Proof ==
Let $\norm {\, \cdot \,}_\infty$ be the supremum norm on $\map \CC {K, \R}$. 
From the Weierstrass Approximation Theorem, there exists a sequence of polynomials $\sequence {p_n}_{n \mathop \in \N}$ such that:
:$\norm {p_n - f}_\infty \to 0$ as $n \to \infty$.
We have:
:$\map {p_n} 0 \to \map f 0 = 0$ as $n \to \infty$.
Take:
:$\map {q_n} x = \map {p_n} x - \map {p_n} 0$
We then have $\map {q_n} 0 = 0$ for each $n \in \N$ and $q_n \to f$ in $\struct {\map \CC {\map {\sigma_A} x, \R}, \norm {\, \cdot \,}_\infty}$.
Since $I$ is an ideal, we have $x^n \in I$ for each $n \ge 1$. 
Since $I$ is a vector subspace, we have $\map {q_n} x \in I$ for each $n \in \N$.
Since the continuous functional calculus is an isometry, we have:
:$\norm {\map {q_n} x - \map f x} = \norm {q_n - f}_\infty \to 0$ as $n \to \infty$ 
So $\map {q_n} x \to \map f x$ as $n \to \infty$. 
Hence since $I$ is closed, we have $\map f x \in I$ as $n \to \infty$. 
Category:Continuous Functional Calculus
Category:Real-Valued Continuous Function Vanishing at Zero applied to Hermitian Element of Closed Ideal of Unital C*-Algebra is contained in Ideal
Real-Valued Continuous Function Vanishing at Zero applied to Hermitian Element of Closed Ideal of Unital C*-Algebra is contained in Ideal/Corollary

== Corollary ==
Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra.
Let $\struct {A_+, \ast, \norm {\, \cdot \,} }$ be the unitization of $\struct {A, \ast, \norm {\, \cdot \,} }$.
Let $A_0 = \set {\tuple {a, 0} : a \in A}$.
Let $x \in A$ be Hermitian.
Let $\map {\sigma_{A_+} } {\tuple {x, 0} } \subseteq \R$ be the spectrum of $\tuple {x, 0}$ in $A$.
Let $f : \map {\sigma_{A_+} } x \to \R$ be a continuous function with $\map f 0 = 0$.
Let $\map f {\tuple {x, 0} }$ be obtained from the continuous functional calculus.
Then $\map f {\tuple {x, 0} } \in A_0$.
Hence there exists $u \in A$ such that $\map f {\tuple {x, 0} } = \tuple {u, 0}$. 
== Proof ==
From Normed Algebra Embeds into Unitization as Closed Ideal, $A_0$ is a closed ideal of $A$.
Since $\tuple {x, 0}^\ast = \tuple {x^\ast, 0} = \tuple {x, 0}$, $\tuple {x, 0}$ is Hermitian in $A_+$.
The result then follows from Real-Valued Continuous Function Vanishing at Zero applied to Hermitian Element of Closed Ideal of Unital C*-Algebra is contained in Ideal.
Category:Real-Valued Continuous Function Vanishing at Zero applied to Hermitian Element of Closed Ideal of Unital C*-Algebra is contained in Ideal
Real-Valued Continuous Function with Compact Support is Uniformly Continuous

== Theorem ==
Let $f : \R \to \R$ be a continuous function such that:
:the support $\map \supp f$ is compact.
Then $f$ is uniformly continuous.
== Proof ==
Since $\map \supp f$ is compact, we can take $\alpha > 0$ such that:
:$\map \supp f \subseteq \closedint {-\alpha} \alpha$
and $\map f x = 0$ for $\cmod x \ge \alpha$. 
From the Heine-Cantor Theorem, $f$ is uniformly continuous on $\closedint {-\alpha - 1} {\alpha + 1}$.
Let $\epsilon > 0$.
Then there exists $\delta' > 0$ such that for $x, y \in \closedint {-\alpha - 1} {\alpha + 1}$ with $\size {x - y} < \delta$ we have:
:$\size {\map f x - \map f y} < \epsilon$ 
Take $\delta = \min \set {\delta', 1/2}$.
Take $x, y \in \R$ with $\size {x - y} < \delta'$. 
If $x, y \in \closedint {-\alpha - 1} {\alpha + 1}$, we have $\size {\map f x - \map f y} < \epsilon$ since $\size {x - y} < \delta' \le \delta$. 
Suppose that $x \in \closedint {-\alpha - 1} {\alpha + 1}$ but $y \in \R \setminus \closedint {-\alpha - 1} {\alpha + 1}$.
Then either $y > \alpha + 1$, in which case $x > \alpha + 1/2$ since $\size {x - y} > 1/2$.
Similarly, if $y < -\alpha - 1$, then $x < -\alpha - 1/2$. 
In either case, $x \in \R \setminus \closedint {-\alpha} \alpha$, so $\map f x = 0$.
Then $\map f x = \map f y = 0$, so $\size {\map f x - \map f y} = 0 < \epsilon$ in this case. 
Hence for all $x, y \in \R$ with $\size {x - y} < \delta$, we have $\size {\map f x - \map f y} < \epsilon$.
So $f$ is uniformly continuous.
Category:Uniformly Continuous Real Functions
Real-Valued Function on Finite Set is Bounded

== Theorem ==
Let $S$ be a finite set.
Let $f: S \to \R$ be a real-valued function on $S$.
Then $f$ is bounded.
== Proof ==
Let $K$ be defined as:
:$K = \ds \max_{x \mathop \in S} \size {\map f x}$
where $\size {\map f x}$ denotes the absolute value of $\map f x$.
Then trivially:
:$\exists K \in \R_{\ge 0}: \forall x \in S: \size {\map f x} \le K$
This is the definition of a bounded real-valued function.
== Sources ==
* : $5$: Compact spaces: $5.1$: Motivation: Step $1$
Category:Bounded Real-Valued Functions
Category:Real-Valued Functions
Category:Finite Sets
Real-Valued Mapping is Continuous if Inverse Images of Unbounded Open Intervals are Open

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space.
Let the real number line $\R$ be considered as a topology under the usual (Euclidean) topology.
Let $f: T \to \R$ be a real-valued function on $T$.
Then:
:$f$ is continuous
:for all $a \in \R$: $f^{-1} \openint \gets a$ and $f^{-1} \openint a \to$ are open in $T$.
== Proof 1 ==
== Proof 2 ==
== Sources ==
* : $3$: Continuity generalized: topological spaces: Exercise $3.9: 7$
Category:Continuous Real-Valued Functions
Category:Real-Valued Mapping is Continuous if Inverse Images of Unbounded Open Intervals are Open
Real-Valued Mapping is Continuous if Inverse Images of Unbounded Open Intervals are Open/Proof 1

== Theorem ==
== Proof ==
=== Sufficient Condition ===
Let $f$ be a continuous mapping.
From the corollary to Open Real Interval is Open Set, both $\openint \gets a$ and $\openint a \to$ are open in $\R$.
Then by definition of continuous mapping, $f^{-1} \openint \gets a$ and $f^{-1} \openint a \to$ are both open in $T$.
=== Necessary Condition ===
Let $f$ be such that:
:for all $a \in \R$: $f^{-1} \openint \gets a$ and $f^{-1} \openint a \to$ are open in $T$.
Let $a, b \in \R$ be arbitrary.
From Sub-Basis for Real Number Line:
:$\set {\openint \gets a, \openint b \to: a, b \in \R}$ is a sub-basis for $\R$.
Hence:
:$\forall a, b \in \R: \openint \gets a \cap \openint b \to$ is open in $T$.
Let $A = \openint \gets a$ and $B = \openint b \to$.
From Preimage of Intersection under Mapping:
:$f^{-1} \sqbrk {A \cap B} = f^{-1} \sqbrk A \cap f^{-1} \sqbrk B$
We have been given that $T$ is a topological space.
By assertion:
:$f^{-1} \sqbrk A$ and $f^{-1} \sqbrk B$ are open in $T$.
Then:
:$f^{-1} \sqbrk A \cap f^{-1} \sqbrk B$ is open in $T$.
That is:
:$f^{-1} \sqbrk {A \cap B}$ is open in $T$.
But:
:$A \cap B = \openint a b$
Hence:
:$f^{-1} \openint a b$ is open in $T$.
$a$ and $b$ are arbitrary.
Hence the preimage of an open real interval is open in $T$.
Let $\family {U_i}_{i \mathop \in I}$ be a family of open intervals of $\R$.
Then from Preimage of Union under Mapping: Family of Sets:
:$\ds f^{-1} \sqbrk {\bigcup_{i \mathop \in I} U_i} = \bigcup_{i \mathop \in I} f^{-1} \sqbrk {U_i}$
where:
:$\ds \bigcup_{i \mathop \in I} U_i$ denotes the union of $\family {U_i}_{i \mathop \in I}$
:$f^{-1} \sqbrk {U_i}$ denotes the preimage of $U_i$ under $f$.
Each of $U_i$ is an open interval in $\R$.
Hence from above each of $f^{-1} \sqbrk {U_i}$ is open in $T$.
As $T$ is a topological space:
:$\ds f^{-1} \sqbrk {\bigcup_{i \mathop \in I} U_i}$ is open in $T$.
From Open Sets in Real Number Line, the open sets of $\R$ are:
:open intervals
:countable unions of pairwise disjoint open intervals.
It has been shown that all subsets of $\R$ of this form have preimages under $f$ which are open in $T$.
That is:
:$f$ is a continuous mapping.
Category:Real-Valued Mapping is Continuous if Inverse Images of Unbounded Open Intervals are Open
Real-Valued Mapping is Continuous if Inverse Images of Unbounded Open Intervals are Open/Proof 2

== Theorem ==
== Proof ==
From Sub-Basis for Real Number Line:
:$\set {\openint \gets a, \openint b \to: a, b \in \R}$ is a sub-basis for $\R$.
The result follows from Continuity Test using Sub-Basis.
Category:Real-Valued Mapping is Continuous if Inverse Images of Unbounded Open Intervals are Open
Real Addition Identity is Zero

== Theorem ==
The identity of real number addition is $0$:
:$\exists 0 \in \R: \forall x \in \R: x + 0 = x = 0 + x$
=== Corollary ===
== Proof ==
From the definition, the real numbers are the set of all equivalence classes $\eqclass {\sequence {x_n} } {}$ of Cauchy sequences of rational numbers.
Let $x = \eqclass {\sequence {x_n} } {}, y = \eqclass {\sequence {y_n} } {}$, where $\eqclass {\sequence {x_n} } {}$ and $\eqclass {\sequence {y_n} } {}$ are such equivalence classes.
From the definition of real addition, $x + y$ is defined as $\eqclass {\sequence {x_n} } {} + \eqclass {\sequence {y_n} } {} = \eqclass {\sequence {x_n + y_n} } {}$.
Let $\sequence {0_n}$ be such that $\forall i: 0_n = 0$.
Then we have:
Similarly for $\eqclass {\sequence {x_n} } {} + \eqclass {\sequence {0_n} } {}$.
Thus the identity element of $\struct {\R, +}$ is the real number $0$.
== Sources ==
* : Chapter $\text {I}$: Elementary Definitions: $\S 1$. Rings and Fields
* : Chapter $1$: Real Numbers and Functions of a Real Variable: $1.2$ Operations with Real Numbers: $(7)$
Category:Additive Group of Real Numbers
Category:Real Addition
Category:Zero
Real Addition Identity is Zero/Corollary

== Corollary to Real Addition Identity is Zero ==
:$\forall x, y \in \R: x + y = x \implies y = 0$
== Proof ==
== Sources ==
* : Part $\text I$: Prologue: Chapter $1$: Basic Properties of Numbers
* : $1$: Set Theory and Logic: $\S 4$: The Integers and the Real Numbers: Exercise $1 \ \text{(a)}$
Category:Real Addition
Real Addition is Associative

== Theorem ==
The operation of addition on the set of real numbers $\R$ is associative:
:$\forall x, y, z \in \R: x + \paren {y + z} = \paren {x + y} + z$
== Proof ==
From the definition, the real numbers are the set of all equivalence classes $\eqclass {\sequence {x_n} } {}$ of Cauchy sequences of rational numbers.
Let $x = \eqclass {\sequence {x_n} } {}, y = \eqclass {\sequence {y_n} } {}, z = \eqclass {\sequence {z_n} } {}$, where $\eqclass {\sequence {x_n} } {}$, $\eqclass {\sequence {y_n} } {}$ and $\eqclass {\sequence {z_n} } {}$ are such equivalence classes.
From the definition of real addition, $x + y$ is defined as $\eqclass {\sequence {x_n} } {} + \eqclass {\sequence {y_n} } {} = \eqclass {\sequence {x_n + y_n} } {}$.
Thus we have:
== Sources ==
* : Chapter $1$: The Real and Complex Number Systems: $\text{1-2}$ Arithmetical properties of real numbers: Axiom $2$
* : Chapter $\text {I}$: Elementary Definitions: $\S 1$. Rings and Fields
* : Chapter $1$: Real Numbers and Functions of a Real Variable: $1.2$ Operations with Real Numbers: $(2)$
Category:Real Addition
Category:Examples of Associative Operations‎
Category:Real Addition
Category:Examples of Associative Operations‎
Category:Associative Law of Addition
Real Addition is Closed

== Theorem ==
The set of real numbers $\R$ is closed under addition:
:$\forall x, y \in \R: x + y \in \R$
== Proof ==
From the definition, the real numbers are the set of all equivalence classes $\eqclass {\sequence {x_n} } {}$ of Cauchy sequences of rational numbers.
Let $x = \eqclass {\sequence {x_n} } {}, y = \eqclass {\sequence {y_n} } {}$, where $\eqclass {\sequence {x_n} } {}$ and $\eqclass {\sequence {y_n} } {}$ are such equivalence classes.
From the definition of real addition, $x + y$ is defined as:
:$\eqclass {\sequence {x_n} } {} + \eqclass {\sequence {y_n} } {} = \eqclass {\sequence {x_n + y_n} } {}$
We have that $\forall i \in \N: x_i \in \Q, y_i \in \Q$, therefore $x_i + y_i \in \Q$.
So it follows that $\eqclass {\sequence {x_n + y_n} } {} \in \R$.
== Sources ==
* : Chapter $1$: Integral Domains: $\S 2$. Operations: Example $1$
* : Chapter $1$: Axioms for the Real Numbers: $2$. Fields: Example $1$
Category:Real Addition
Category:Algebraic Closure
Real Addition is Commutative

== Theorem ==
The operation of addition on the set of real numbers $\R$ is commutative:
:$\forall x, y \in \R: x + y = y + x$
== Proof ==
From the definition, the real numbers are the set of all equivalence classes $\eqclass {\sequence {x_n} } {}$ of Cauchy sequences of rational numbers.
Let $x = \eqclass {\sequence {x_n} } {}, y = \eqclass {\sequence {y_n} } {}$, where $\eqclass {\sequence {x_n} } {}$ and $\eqclass {\sequence {y_n} } {}$ are such equivalence classes.
Thus:
== Sources ==
* : Chapter $1$: The Real and Complex Number Systems: $\text{1-2}$ Arithmetical properties of real numbers: Axiom $1$
* : Chapter $\text {I}$: Elementary Definitions: $\S 1$. Rings and Fields
* : Chapter $1$: Real Numbers and Functions of a Real Variable: $1.2$ Operations with Real Numbers: $(1)$
Category:Real Addition
Category:Examples of Commutative Operations
Category:Commutative Law of Addition
Real Addition is Computably Uniformly Continuous

== Theorem ==
Let $f : \R^2 \to \R$ be defined as:
:$\map f {x, y} = x + y$
Then $f$ is computably uniformly continuous.
== Proof ==
We will define $d : \N \to \N$ as:
:$\map d n = 2 n + 1$
which is primitive recursive by:
* Addition is Primitive Recursive
* Constant Function is Primitive Recursive
and thus total recursive by:
* Primitive Recursive Function is Total Recursive Function
Let $x_1, y_1, x_2, y_2 \in \R$ and $n \in \N$ be arbitrary, and suppose:
:$\norm {\tuple {x_1, y_1} - \tuple {x_2, y_2}} < \dfrac 1 {\map d n + 1} = \dfrac 1 {2 n + 2}$
We have:
and thus:
:$\size {x_1 - x_2} \le \norm {\tuple {x_1, y_1} - \tuple {x_2, y_2}} < \dfrac 1 {2 n + 2}$
:$\size {y_1 - y_2} \le \norm {\tuple {x_1, y_1} - \tuple {x_2, y_2}} < \dfrac 1 {2 n + 2}$
Hence:
Category:Computability Theory
Real Addition is Well-Defined

== Theorem ==
The operation of addition on the set of real numbers $\R$ is well-defined.
== Proof ==
From the definition, the real numbers are the set of all equivalence classes $\eqclass {\sequence {x_n} } {}$ of Cauchy sequences of rational numbers:
:$\eqclass {\sequence {x_n} } {} \equiv \eqclass {\sequence {y_n} } {} \iff \forall \epsilon > 0: \exists n \in \N: \forall i, j > n: \size {x_i - y_j} < \epsilon$
Let $x = \eqclass {\sequence {x_n} } {}$ and $y = \eqclass {\sequence {y_n} } {}$, where $\eqclass {\sequence {x_n} } {}$ and $\eqclass {\sequence {y_n} } {}$ are such equivalence classes.
From the definition of real addition, $x + y$ is defined as:
:$\eqclass {\sequence {x_n} } {} + \eqclass {\sequence {y_n} } {} = \eqclass {\sequence {x_n + y_n} } {}$.
We need to show that:
:$\sequence {x_n}, \sequence {x'_n} \in \eqclass {\sequence {x_n} } {}, \sequence {y_n}, \sequence {y'_n} \in \eqclass {\sequence {y_n} } {} \implies \sequence {x_n + y_n} = \sequence {x'_n + y'_n}$
That is:
:$\forall \epsilon > 0: \exists N: \forall i, j > N: \size {\paren {x_i + y_i} - \paren {x'_j + y'_j} } < \epsilon$
Let $\epsilon > 0$, such that:
:$\exists N_1: \forall i, j \ge N_1: \size {x_i - x'_j} < \epsilon / 2$
:$\exists N_2: \forall i, j \ge N_2: \size {y_i - y'_j} < \epsilon / 2$
Now let $N = \max \set {N_1, N_2}$.
Then we have:
:$\forall i, j \ge N: \size {x_i - x'_j} + \size {y_i - y'_j} < \epsilon$
But:
So:
:$\forall i, j \ge N: \size {\paren {x_i + y_i} - \paren {x'_j + y'_j} } < \epsilon$
Hence the result.
Category:Real Addition
Real Arccosine/Examples/Sine of Twice Arccosine of x

== Example of Use of Real Arccosine ==
:$\map \sin {2 \arccos x}$
can be simplified to:
:$2 x \sqrt {1 - x^2}$
== Proof ==
Let $\arccos x = \theta$.
Then:
Then:
== Sources ==
* : $\text V$. Trigonometry: Inverse ratios
Category:Examples of Use of Real Arccosine
Real Area Hyperbolic Cosecant of x over a in Logarithm Form

== Theorem ==
For $a > 0$:
:$\arcsch \dfrac x a = \map \ln {\dfrac {a + \sqrt {a^2 + x^2} } {\size x} }$
== Proof ==
We have that $\arcsch \dfrac x a$ is defined whenever $x \ne 0$.
== Also see ==
* $\arsinh \dfrac x a$ in Logarithm Form
* $\arcosh \dfrac x a$ in Logarithm Form
* $\artanh \dfrac x a$ in Logarithm Form
* $\arcoth \dfrac x a$ in Logarithm Form
* $\arsech \dfrac x a$ in Logarithm Form
Category:Inverse Hyperbolic Cosecant
Real Area Hyperbolic Cosine of Reciprocal equals Real Area Hyperbolic Secant

== Theorem ==
Everywhere that the function is defined:
:$\map \arcosh {\dfrac 1 x} = \arsech x$
where $\arcosh$ and $\arsech$ denote real area hyperbolic cosine and real area hyperbolic secant respectively.
== Proof ==
== Sources ==
* : $\S 8$: Hyperbolic Functions: $8.62$: Relations Between Inverse Hyperbolic Functions
Category:Inverse Hyperbolic Secant
Category:Inverse Hyperbolic Cosine
Category:Reciprocals