nyuuzyou/wikis huggingface dataset:
Image of von Neumann-Bounded Set under Equicontinuous Family of Linear Transformations is Contained in von Neumann-Bounded Set

== Theorem ==
Let $\GF \in \set {\R, \C}$. 
Let $X$ and $Y$ be a topological vector space over $\GF$. 
Let $\family {T_\alpha}_{\alpha \in I}$ be an equicontinuous family of linear transformations. 
Let $E \subseteq X$ be von Neumann-bounded. 
Then there exists a von Neumann-bounded set $F \subseteq Y$ such that: 
:$T_\alpha \sqbrk E \subseteq F$ for each $\alpha \in I$. 
== Proof ==
Let:
:$\ds F = \bigcup_{\alpha \mathop \in I} T_\alpha \sqbrk E$
Then $T_\alpha \sqbrk E \subseteq F$ for each $\alpha \in I$.
It is enough to show that $F$ is von Neumann-bounded.
Let $W$ be an open neighborhood of $\mathbf 0_Y$.
Since $\family {T_\alpha}_{\alpha \in I}$ is equicontinuous, there exists an open neighborhood $V$ of $\mathbf 0_X$ such that: 
:$T_\alpha \sqbrk V \subseteq W$ for each $\alpha \in I$. 
Since $E$ is von Neumann-bounded, there exists $s > 0$ such that for all $t > s$ we have $E \subseteq t W$. 
Then for each $t > s$ and $\alpha \in I$, we have:
So, from Union of Subsets is Subset:
:$\ds F = \bigcup_{\alpha \in I} T_\alpha \sqbrk E \subseteq t W$
for $t > s$.
So $F$ is von Neumann-bounded.
== Sources ==
* : $2.4$: Equicontinuity
Category:Equicontinuous Families of Linear Transformations between Topological Vector Spaces
Category:von Neumann-Bounded Subsets of Topological Vector Spaces
Image under Epimorphism of Center is Subset of Center

== Theorem ==
Let $G$ and $H$ be groups.
Let $\theta: G \to H$ be an epimorphism.
Let $\map Z G$ denote the center of $G$.
Then:
:$\theta \sqbrk {\map Z G} \subseteq \map Z H$
== Proof ==
Let $y \in \theta \sqbrk {\map Z G}$.
Let $t \in H$.
We have that:
:$y = \map \theta z$
for some $z \in \map Z G$
As $\theta$ is an epimorphism, it is by definition surjective.
Then:
:$t = \map \theta s$
for some $s \in G$.
Hence:
As $t$ is arbitrary, it follows that $y \in \map Z H$.
The result follows.
== Sources ==
* : Chapter $8$: Homomorphisms, Normal Subgroups and Quotient Groups: Exercise $6$
Category:Centers of Groups
Category:Group Epimorphisms
Image under Inclusion Mapping

== Theorem ==
Let $X$ be a set.
Let $S \subseteq X$, $Z \subseteq S$.
Then $i_S \sqbrk Z = Z$
where
:$i_S$ denotes the inclusion mapping of $S$
:$i_S \sqbrk Z$ denotes the image of $Z$ under $i_S$.
== Proof ==
== Sources ==
* 
Category:Inclusion Mappings
Image under Increasing Mapping equal to Special Set is Complete Lattice

== Theorem ==
Let $L = \struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $f: S \to S$ be an increasing mapping.
Let $P = \struct {M, \precsim}$ be an ordered subset of $L$ such that
:$M = \set {x \in S: x = \map f x}$
Then $P$ is complete lattice.
== Proof ==
We will prove that
:$\forall X \subseteq M: \forall Y \subseteq S: Y = \left\{ {x \in S: x}\right.$ is upper bound for $\left.{X \land \map f x \preceq x}\right\} \implies \inf_L Y \in M$
Let $X \subseteq M$, $Y \subseteq S$ such that
:$Y = \left\{ {x \in S: x}\right.$ is upper bound for $\left.{X \land \map f x \preceq x}\right\}$
We will prove that
:$\map f {\inf Y}$ is lower bound for $Y$.
Let $y \in Y$.
By definition of $Y$:
:$\map f y \preceq y$
By definitions of infimum and lower bound:
:$\inf Y \preceq y$
By definition of increasing mapping:
:$\map f {\inf Y} \preceq \map f y$
Thus by definition of transitivity:
:$\map f {\inf Y} \preceq y$
We will prove that
:$\map f {\map f {\inf Y} }$ is upper bound for $X$.
Let $m \in X$.
We will prove that
:$m$ is lower bound for $Y$.
Let $y \in Y$.
By definition of $Y$:
:$\map f y$ is upper bound for $X$ and $\map f y \preceq y$
By definition of upper bound:
:$m \preceq \map f y$
Thus by definition of transitivity:
:$m \preceq y$
By definition of infimum:
:$m \preceq \inf Y$
By definition of increasing mapping:
:$\map f m \preceq \map f {\inf Y}$
By definition of subset:
:$m \in M$
By definition of $M$:
:$m = \map f m$
By definition of increasing mapping:
:$m \preceq \map f {\map f {\inf Y} }$
By definition of infimum:
:$\map f {\inf Y} \preceq \inf Y$
By definition of increasing mapping:
:$\map f {\map f {\inf Y} } \preceq \map f {\inf Y}$
By definition of $Y$:
:$\map f {\inf Y} \in Y$
By definitions of infimum and lower bound:
:$\inf Y \preceq \map f {\inf Y}$
By definition of antisymmetry:
:$\inf Y = \map f {\inf Y}$
Thus by definition of $M$:
:$\inf Y \in M$
Define:
:$Y_0 = \left\{ {y \in S: \map f y}\right.$ is upper bound for $\left.{M \land \map f y \preceq y}\right\}$
By lemma:
:$\inf Y_0 \in M$
We will prove that
:$\forall X \subseteq M: X$ admits a supremum in $P$.
Let $X \subseteq M$.
Define:
:$Y = \left\{ {y \in S: \map f y}\right.$ is upper bound for $\left.{M \land \map f y \preceq y}\right\}$
Define $z = \inf Y$.
By lemma:
:$z \in M$
We will prove that
:$z$ is upper bound for $X$ in $P$.
Let $m \in X$.
By analogy:
:$m$ is lower bound for $Y$ in $L$.
By definition of infimum:
:$m \preceq \inf Y$
Thus by definition of ordered subset:
:$m \precsim z$
We will prove that
:$\forall x \in M: x$ is upper bound for $X$ in $P \implies z \precsim x$
Let $x \in M$ such that
:$x$ is upper bound for $X$.
By definition of $M$:
:$x = \map f x$
By definition of ordered subset:
:$\map f x$ is upper bound for $X$ in $L$.
By definition of $Y$:
:$x \in Y$
By definitions of infimum and lower bound:
:$\inf Y \preceq x$
Thus by definition of ordered subset:
:$z \precsim x$
Hence $X$ admits a supremum in $P$.
Thus by {{Complete iff Admits All Suprema]]:
:$P$ is a complete lattice.
== Sources ==
* 
Category:Complete Lattices
Image under Left-Total Relation is Empty iff Subset is Empty

== Theorem ==
Let $\RR \subseteq S \times T$ be a left-total relation.
Let $A \subseteq S$.
Then:
:$\RR \sqbrk A = \O$ $A = \O$
== Proof ==
=== Necessary Condition ===
We prove the contrapositive statement:
:$A \ne \O \implies \RR \sqbrk A \ne \O$
Let $s \in A$.
By definition of left-total relation:
:$\exists t \in T : \tuple{s, t} \in \RR$
By definition of image:
:$\exists t \in T : t \in \RR \sqbrk A$
Hence:
:$\RR \sqbrk A \ne \O$
The result follows from Rule of Transposition.
=== Sufficient Condition ===
Follows immediately from Image of Empty Set is Empty Set.
Category:Composite Relations
Image under Projection from Closed Set of Product Topology is not necessarily Closed

== Theorem ==
Let $T_1 = \struct {S_1, \tau_1}$ and $T_2 = \struct {S_2, \tau_2}$ be topological spaces.
Let $T = \struct {T_1 \times T_2, \tau}$ be the product space of $T_1$ and $T_2$, where $\tau$ is the product topology on $S$.
Let $\pr_1: T \to T_1$ and $\pr_2: T \to T_2$ be the first and second projections from $T$ onto its factors.
Let $K \subseteq S_1 \times S_2$ be closed in $T$.
Then $\pr_1 \sqbrk K$ is not necessarily closed in $T_1$.
== Proof ==
Proof by Counterexample:
Let $K = \set {\tuple {x, y} \in \R^2: x \ge 0, y \ge \dfrac 1 x}$
Then:
:$\pr_1 \sqbrk K = \openint 0 \to$
$K$ is closed in $T$, as follows:
Consider the mapping $f: \R^2 \to \R$ defined as:
:$\map f {x, y} = x y$
which is continuous on $\R^2$ (see Preimages of $\map f {x, y} = \tuple {x^2 + y^2, x y}$: Continuity).
Then we note that:
$K = f^{-1} \hointr 1 \to \cap p_1^{-1} \hointr 0 \to$
and the result follows.
== Also see ==
* Projection from Product Topology is Continuous
== Sources ==
* : $3$: Continuity generalized: topological spaces: Exercise $3.9: 34 \ \text {(b)}$
Category:Product Topology
Category:Open Mappings
Category:Projections
Category:Projection from Product Topology is Open and Continuous
Image under Subset of Relation is Subset of Image under Relation

== Theorem ==
Let $S$ and $T$ be sets.
Let $\RR_1 \subseteq S \times T$ be a relation in $S \times T$.
Let $\RR_2 \subseteq \RR_1$.
Let $A \subseteq S$.
Then:
:$\RR_2 \sqbrk A \subseteq \RR_1 \sqbrk A$
where $\RR_1 \sqbrk A$ denotes the image of $A$ under $\RR_1$.
=== Corollary ===
== Proof ==
== Sources ==
* : Chapter $0$: Relations
Category:Relation Theory
Image under Subset of Relation is Subset of Image under Relation/Corollary

== Theorem ==
Let $S$ and $T$ be sets.
Let $\RR_1 \subseteq S \times T$ be a relation in $S \times T$.
Let $\RR_2 \subseteq \RR_1$.
Let $x \in S$.
Then:
:$\map {\RR_2} x \subseteq \map {\RR_1} x$
where $\map {\RR_1} x$ denotes the image of $x$ under $\RR_1$.
== Proof ==
Category:Relation Theory
Images of Elements under Repeated Composition of Injection form Equivalence Classes

== Theorem ==
Let $S$ be a set.
Let $f: S \to S$ be an injection.
Let the sequence of mappings:
:$f^0, f^1, f^2, \ldots, f^n, \ldots$
be defined as:
:$\forall n \in \N: \map {f^n} x = \begin {cases}
x & : n = 0 \\
\map f x & : n = 1 \\
\map f {\map {f^{n - 1} } x} & : n > 1
\end {cases}$
Let $\RR \subseteq S \times S$ be the relation on $S$ defined as:
:$\RR = \set {\tuple {a, b} \in S \times S: \exists k \in \Z: b = \map {f^k} a \lor \exists j \in \Z: a = \map {f^j} b}$
Then $\RR$ is an equivalence relation.
== Proof ==
Checking in turn each of the criteria for equivalence:
=== Reflexivity ===
By definition, $f^0$ is the identity mapping.
So by definition of $f^0$:
:$\forall a \in S: a = \map {f^0} a$
That is:
:$a \mathrel \RR a$
So $\RR$ has been shown to be reflexive.
=== Symmetry ===
Let $a \mathrel \RR b$.
That is:
:$b = \map {f^k} a$
for some $k \in \Z$.
Let $g_k$ be the restriction of $f^k$ to its image.
From Injection to Image is Bijection, $g^k$ is a bijection.
From Inverse of Bijection is Bijection:
:$\map {\paren {g^k}^{-1} } b = a$
Consider the extension $\paren {f^k}^{-1}$ of $\paren {g^k}^{-1}$ to its codomain which is $S$.
From Inverse of Injection is Many-to-One Relation, $\map {\paren {f^k}^{-1} } b = a$ is well-defined.
By interpreting $\map {\paren {f^k}^{-1} } b = a$ as $\map {f^{-k} } b = a$, it follows that we can set $j = -k$ and so:
:$\exists j \in \Z: \map {f^j} b = a$
That is:
:$b \mathrel \RR a$
So $\RR$ has been shown to be symmetric.
=== Transitivity ===
Let $a \mathrel \RR b$ and $b \mathrel \RR c$.
That is:
:$b = \map {f^{k_1} } a$
:$c = \map {f^{k_2} } b$
where $k_1, k_2 \in \Z$.
That is:
:$c = \map {f^{k_2} } {\map {f^{k_1} } a}$
By Composition of Repeated Compositions of Injections:
:$c = \map {f^{k_2} } {\map {f^{k_1} } a} = \map {f^{k_1 + k_2} } a$
and so:
:$a \mathrel \RR c$
So $\RR$ has been shown to be transitive.
$\RR$ has been shown to be reflexive, symmetric and transitive.
Hence by definition it is an equivalence relation.
== Sources ==
* : Chapter $1$: Theory of Sets: $\S 7$: Relations: Exercise $3$
Category:Injections
Category:Composite Mappings
Imaginary Numbers under Addition form Group

== Theorem ==
Let $\II$ denote the set of complex numbers of the form $0 + i y$
That is, let $\II$ be the set of all wholly imaginary numbers.
Then the algebraic structure $\struct {\II, +}$ is a group.
== Proof ==
We have that $\II$ is a non-empty subset of the complex numbers $\C$.
Indeed, for example:
:$0 + 0 i \in \II$
Now, let $0 + i x, 0 + i y \in \II$.
Then we have:
Hence the result by the One-Step Subgroup Test.
== Sources ==
* : Chapter $\text{II}$: Groups: Exercise $\text{B i}$
Category:Complex Addition
Category:Examples of Groups
Imaginary Numbers under Multiplication do not form Group

== Theorem ==
Let $\II$ denote the set of complex numbers of the form $0 + i y$ for $y \in \R_{\ne 0}$.
That is, let $\II$ be the set of all wholly imaginary non-zero numbers.
Then the algebraic structure $\struct {\II, \times}$ is not a group.
== Proof ==
Let $0 + i x \in \II$.
We have:
So $\struct {\II, \times}$ is not closed.
Hence $\struct {\II, \times}$ is not a group.
== Sources ==
* : Chapter $\text{II}$: Groups: Exercise $\text{B ii}$
Category:Complex Multiplication
Imaginary Part as Mapping is Endomorphism for Complex Addition

== Theorem ==
Let $\struct {\C, +}$ be the additive group of complex numbers.
Let $\struct {\R, +}$ be the additive group of real numbers.
Let $f: \C \to \R$ be the mapping from the complex numbers to the real numbers defined as:
:$\forall z \in \C: \map f z = \map \Im z$
where $\map \Im z$ denotes the imaginary part of $z$.
Then $f: \struct {\C, +} \to \struct {\R, +}$ is a group epimorphism.
Its kernel is the set:
:$\map \ker f = \R$
of (wholly) real numbers.
== Proof ==
From Imaginary Part as Mapping is Surjection, $f$ is a surjection.
Let $z_1, z_2 \in \C$.
Let $z_1 = x_1 + i y_1, z_2 = x_2 + i y_2$.
Then:
So $f$ is a group homomorphism.
Thus $f$ is a surjective group homomorphism and therefore by definition a group epimorphism.
Finally:
:$\forall y \in \R: \map \Im {x + 0 i} = 0 i = 0$
It follows from Complex Addition Identity is Zero that: 
:$\map \ker f = \set {x: x \in \R} = \R$
== Also see ==
* Real Part as Mapping is Endomorphism for Complex Addition
== Sources ==
* : Chapter $\text {II}$: New Structures from Old: $\S 12$: Homomorphisms: Example $12.3$
* : Chapter $\text{II}$: Groups: Direct Products
Category:Complex Addition
Category:Group Endomorphisms
Category:Imaginary Parts
Imaginary Part as Mapping is Surjection

== Theorem ==
Let $f: \C \to \R$ be the projection from the complex numbers to the real numbers defined as:
:$\forall z \in \C: \map f z = \map \Im z$
where $\map \Im z$ denotes the imaginary part of $z$.
Then $f$ is a surjection.
== Proof ==
Let $y \in \R$ be a real number.
Let $x \in \R$ be an arbitrary real number.
Let $z \in \C$ be the complex number defined as:
:$z = x + i y$
Then we have:
:$\map \Im z = y$
That is:
:$\exists z \in \C: \map f z = y$
The result follows by definition of surjection.
== Also see ==
* Real Part as Mapping is Surjection
== Sources ==
* : Chapter $\text{II}$: Groups: Direct Products
Category:Imaginary Parts
Category:Examples of Surjections
Imaginary Part of Complex Exponential Function

== Theorem ==
Let $z = x + i y \in \C$ be a complex number, where $x, y \in \R$.
Let $\exp z$ denote the complex exponential function.
Then:
:$\map \Im {\exp z} = e^x \sin y$
where:
:$\map \Im z$ denotes the imaginary part of a complex number $z$
:$e^x$ denotes the real exponential function of $x$
:$\sin y$ denotes the real sine function of $y$.
== Proof ==
From the definition of the complex exponential function:
:$\exp z := e^x \paren {\cos y + i \sin y}$
The result follows by definition of the imaginary part of a complex number.
== Sources ==
* : $\S 4.5$. The Functions $e^z$, $\cos z$, $\sin z$
Category:Exponential Function
Imaginary Part of Complex Product

== Theorem ==
Let $z_1$ and $z_2$ be complex numbers.
Then:
:$\map \Im {z_1 z_2} = \map \Re {z_1} \, \map \Im {z_2} + \map \Im {z_1} \, \map \Re {z_2}$
== Proof ==
Let $z_1 = x_1 + i y_1$ and $z_2 = x_2 + i y_2$.
By definition of complex multiplication:
:$z_1 z_2 = x_1 x_2 - y_1 y_2 + i \paren {x_1 y_2 + x_2 y_1}$
Then
== Sources ==
* : $1$: Complex Numbers: Supplementary Problems: Miscellaneous Problems: $166 \ \text{(b)}$
Category:Complex Multiplication
Imaginary Part of Element of *-Algebra is Real Linear

== Theorem ==
Let $\struct {A, \ast}$ be a $\ast$-algebra over $\C$.
Let $x, y \in A$ and $\lambda \in \R$.
Then we have:
:$\map \Im {x + \lambda y} = \map \Im x + \lambda \map \Im y$
where $\Im$ denotes real part. 
== Proof ==
We have:
Category:*-Algebras
Imaginary Part of Imaginary Unit times Element of *-Algebra

== Theorem ==
Let $\struct {A, \ast}$ be a $\ast$-algebra over $\C$.
Let $x \in A$.
Then:
:$\map \Im {i x} = \map \Re x$
where $\Re$ and $\Im$ denote the real and imaginary parts of $A$.
== Proof ==
We have:
Category:*-Algebras
Imaginary Part of Integer Power of Complex Number is Harmonic

== Theorem ==
Let $z \in \C$ be a complex number.
Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Let $z^n$ denote $z$ raised to the $n$th power.
Then the imaginary part $\map \Im {z^n}$ of $z^n$ is a harmonic polynomial.
== Proof ==
Let $z = x + i y$.
Then:
Then we have:
and:
It remains to be shown that for $j \in \set {0, 1, \ldots, n - 2}$ that:
:$\paren {-1}^{\paren {j - 1} / 2} \dbinom n j \paren {n - j} \paren {n - j - 1} = -\paren {-1}^{\paren {j + 1} / 2} \dbinom n {j + 2} \paren {j + 2} \paren {j + 1}$
First we have that:
Hence it remains to be shown that:
:$\dbinom n j \paren {n - j} \paren {n - j - 1} = \dbinom n {j + 2} \paren {j + 2} \paren {j + 1}$
We have:
and:
Hence the result.
== Sources ==
* : $3$: Elementary Analytic Methods: $3.7$ Complex Numbers and Functions: Powers: $3.7.23$
Category:Imaginary Parts
Category:Harmonic Polynomials
Category:Complex Powers
Imaginary Part of Linear Functional is Linear Functional

== Theorem ==
Let $X$ be a vector space over $\C$. 
Let $f : X \to \C$ be a linear functional. 
Define $h : X \to \R$ by: 
:$\map h x = \map \Im {\map f x}$
for each $x \in X$.
Then $f$ is $\R$-linear. 
== Proof ==
Let $x, y \in X$ and $\lambda, \mu \in \R$. 
Then:
Category:Linear Functionals
Imaginary Part of Sine of Complex Number

== Theorem ==
Let $z = x + i y \in \C$ be a complex number, where $x, y \in \R$.
Let $\sin z$ denote the complex sine function.
Then:
:$\Im \paren {\sin z} = \cos x \sinh y$
where:
:$\Im z$ denotes the imaginary part of a complex number $z$
:$\sin$ denotes the complex sine function
:$\cos$ denotes the real cosine function
:$\sinh$ denotes the hyperbolic sine function.
== Proof ==
From Sine of Complex Number:
:$\sin \paren {x + i y} = \sin x \cosh y + i \cos x \sinh y$
The result follows by definition of the imaginary part of a complex number.
== Sources ==
* : $\S 4.5$. The Functions $e^z$, $\cos z$, $\sin z$
Category:Sine Function
Imaginary Unit to Power of Itself

== Theorem ==
:$i^i = e^{-\pi / 2}$
where $i$ is the imaginary unit.
Its decimal expansion is:
:$0 \cdotp 20787 \, 95763 \, 50761 \, 90854 \, 6955 \ldots$
=== Complete Result ===
The full result is actually more complicated than that:
== Proof ==
== Sources ==
* : $0,20787 95763 50761 \ldots$
* : $0 \cdotp 207 \, 879 \, 576 \, 350 \, 761 \, 908 \, 546 \, 955 \ldots$
* : Chapter $\text {A}.21$: Euler (): Footnote $2$
* : $0 \cdotp 20787 \, 95763 \, 50761 \, 90854 \, 6955 \ldots$
Category:Imaginary Unit to Power of Itself
Category:Imaginary Unit
Imaginary Unit to Power of Itself/Complete

== Theorem ==
:$i^i = \set {\exp \paren {\dfrac {4 k + 3} 2 \pi}: k \in \Z}$
where $i$ is the imaginary unit.
== Proof ==
== Also presented as ==
This result can also be presented as:
:$i^i = \set {\exp \paren {- \dfrac \pi 2 \paren {4 k + 1} }: k \in \Z}$
== Sources ==
* : $\S 4$. Elementary Functions of a Complex Variable: Exercise $6 \ \text{(iv)}$
* : Chapter $\text {A}.21$: Euler (): Footnote $2$
Category:Imaginary Unit to Power of Itself
Immediate Predecessor under Total Ordering is Unique

== Theorem ==
Let $\preceq$ be a total ordering.
Let $a$ be an immediate predecessor to $b$.
Then $a$ is unique.
That is, if $a$ and $a'$ are both immediate predecessors to $b$, then $a = a'$.
== Proof ==
Let $a$ and $a'$ both be immediate predecessors of $b$.
We have that $\preceq$ is a total ordering.
, suppose:
:$a \preceq a'$
By virtue of $a$ being a immediate predecessor of $b$:
:$\neg \exists c \in S: a \prec c \prec b$
However, since $a'$ is also an immediate predecessor:
:$a' \prec b$
Hence, it cannot be the case that $a \prec a'$.
Since $a \preceq a'$, it follows that $a = a'$.
Hence the result.
== Also see ==
* Immediate Successor under Total Ordering is Unique
== Sources ==
* : $1$: Set Theory and Logic: $\S 3$: Relations: Exercise $3.11$
* : Chapter $4$: Superinduction, Well Ordering and Choice: Part $\text I$ -- Superinduction and Well Ordering: $\S 1$ Introduction to well ordering: Proposition $1.3$
Category:Total Orderings
Category:Predecessor Elements
Immediate Successor is Unique in Toset

== Theorem ==
Let $(S, \preceq)$ be a totally ordered set.
Let $x, y \in S$.
Suppose that $y$ is an immediate successor of $x$.
Then $y$ is the only immediate successor of $x$.
== Proof ==
 that $x$ has another immediate successor, $z ≠ y$.
Then by definition:
:$x \prec y$
:$x \prec z$
Since $\preceq$ is a total ordering and $y ≠ z$:
:$y \prec z$ or $z \prec y$.
If $y \prec z$ then $x \prec y \prec z$, contradicting the fact that $z$ is an immediate successor of $x$.
If $z \prec y$ then $x \prec z \prec y$, contradicting the fact that $y$ is an immediate successor of $x$.
Thus we conclude that there can be no such $z$.
== Sources ==
* : Proposition $4.1.3$
Category:Total Orderings
Immediate Successor under Total Ordering is Unique

== Theorem ==
Let $\preceq$ be a total ordering.
Let $b$ be an immediate successor to $a$.
Then $b$ is unique.
That is, if $b$ and $b'$ are both immediate successor to $a$, then $b = b'$.
== Proof ==
Let $b$ and $b'$ both be immediate successors to $a$.
We have that $\preceq$ is a total ordering.
:
:$b \preceq b'$
By virtue of $b'$ being a immediate successor of $a$:
:$\neg \exists c \in S: a \prec c \prec b'$
However, since $b$ is also an immediate successor:
:$a \prec b$
Hence, it cannot be the case that $b \prec b'$.
Since $b \preceq b'$, it follows that $b = b'$.
Hence the result.
== Also see ==
* Immediate Predecessor under Total Ordering is Unique
== Sources ==
* : $1$: Set Theory and Logic: $\S 3$: Relations: Exercise $3.11$
* : Chapter $4$: Superinduction, Well Ordering and Choice: Part $\text I$ -- Superinduction and Well Ordering: $\S 1$ Introduction to well ordering: Proposition $1.3$
Category:Total Orderings
Category:Successor Elements
Implications of Stokes' Theorem

== Theorem ==
Stokes' Theorem implies all of the following results:
* Classical Stokes' Theorem
* Green's Theorem
* Gauss's Theorem
* Fundamental Theorem of Calculus
* Cauchy's Residue Theorem
== Proof ==
=== Classical Stokes' Theorem ===
We note that given $f_1, f_2, f_3: \R^3 \to \R$, $f_1 \rd x + f_2 \rd y + f_3 \rd z$ is a $1$-form defined on a surface.
Since we are integrating over the boundary of a surface, which is a $1$-manifold, we may use the general Stokes' theorem:
If we define $\mathbf F: \R^3 \to \R^3$ as:
:$\mathbf F = f_1 \mathbf e_1 + f_2 \mathbf e_2 + \mathbf e_3$
we recognize this expression as:
:$\nabla \times \mathbf F$
with:
:$\d y \wedge \d z$ replacing $\mathbf e_1$
:$\d z \wedge \d x$ replacing $\mathbf e_2$
and:
:$\d x \wedge \d y$ replacing $\mathbf e_3$.
=== Green's Theorem ===
We note that given $A, B: \R^2 \to \R$, $A \rd x + B \rd y$ is a $1$-form defined on some open set $U \subset \R^2$.
Since we are integrating a $1$-form on $\partial U$, a $1$-manifold, we may use the general Stokes' theorem: 
=== Divergence Theorem ===
We note that the expression $\mathbf F \cdot \mathbf n \rd S$ is a $2$-form, since it takes two vectors ($F$ and $n$) and outputs a scalar.
Less formally:
:$\mathbf F \cdot \mathbf n \rd S = $ (scalar)(area $2$-form) $=$ $2$-form
Since we are integrating this expression over the boundary of a region in three space, which is a $2$-manifold, we may use the general Stokes' theorem:
=== Fundamental Theorem of Calculus ===
Given a function $f: \R \to \R$, integrable on some open set $I$, we can recognize such a function a $0$-form -- that is, defined at a point and taking no vectors as inputs.
Hence the exterior derivative is just the ordinary differential:
:$\map {f'} x \rd x$
Since the ordinary differential is a $1$-form, and we are integrating on a $1$-manifold, we may use the general Stokes' theorem:
:$\ds \int_I \map f x \rd x = \int_{\partial I} \map f x$
By Induced Orientations on Boundaries, $\partial I = \set {x_0', x_1}$ for some points $x_0, x_1$ where $y'$ indicates a point with "negative" orientation.
We then have
:$\ds \int_{\partial I} \map f x = -\map f {x_0} + \map f {x_1} = \map f {x_1} - \map f {x_0}$
=== Cauchy's Residue Theorem ===
Let $z = x + iy$ and $\map f z = \map u {x, y} + i \map v {x, y}$ for two real functions $u, v$.
Let $D$ be a disk and its boundary $\partial D = C$ a circle.
Then by Stokes' Theorem:
:$\ds \int_C \map f z \rd z = \int_C \map u z \rd x + \map v z \rd y = \int_D \frac {\partial u} {\partial y} - \frac {\partial v} {\partial x}$ 
which is zero if $f$ satisfies the Cauchy-Riemman conditions.
Category:Calculus