nyuuzyou/wikis huggingface dataset:
Manipulation of Absolutely Convergent Series/Scale Factor

== Theorem ==
Let $\ds \sum_{n \mathop = 1}^\infty a_n$ be a real or complex series that is absolutely convergent.
Let $c \in \R$, or $c \in \C$.
Then:
:$\ds c \sum_{n \mathop = 1}^\infty a_n = \sum_{n \mathop = 1}^\infty c a_n$
== Proof ==
Category:Series
Category:Convergence
Manipulation of Exterior Derivative

== Theorem ==
For the exterior derivative, the following statements are true:
:$\map \d {a b} = a \rd b + \paren {\d a} b$
:$\map \d {a \wedge b} = \d a \wedge b - a \wedge \d b$
where $a \wedge b$ is the wedge product.
== Proof ==
Category:Topology
Many-to-One Relation/Examples/Square

== Example of Many-to-One Relation ==
Let $\RR \subseteq \R \times \R$ be the relation on $\R$ defined as:
:$\forall \tuple {x, y} \in \R \times \R: \tuple {x, y} \in \RR \iff x^2 = y$
Then $\RR$ is a many-to-one relation
== Proof ==
Let:
:$y_1, y_2 \in \R: \tuple {x, y_1} \in \RR \land \tuple {x, y_2} \in \RR$
Then:
:$y_1 = x^2 = y_2$
and so:
:$y_1 = y_2$
Hence the result.
== Sources ==
* 
Category:Examples of Many-to-One Relations
Many-to-One Relation Composite with Inverse is Transitive

== Theorem ==
Let $\RR \subseteq S \times T$ be a relation which is many-to-one.
Then the composites (both ways) of $\RR$ and its inverse $\RR^{-1}$, that is, both $\RR^{-1} \circ \RR$ and $\RR \circ \RR^{-1}$, are transitive.
== Proof ==
Let $\RR \subseteq S \times T$ be many-to-one.
Then, from the definition of many-to-one:
:$\RR \subseteq S \times T: \forall x \in S: \tuple {x, y_1} \in \RR \land \tuple {x, y_2} \in \RR \implies y_1 = y_2$
Also, note that from Inverse of Many-to-One Relation is One-to-Many, $\RR^{-1}$ is one-to-many.
Let $\tuple {a, b}, \tuple {b, c} \in \RR^{-1} \circ \RR$.
Thus $\RR^{-1} \circ \RR$ is transitive.
Now let $\tuple {p, q}, \tuple {q, r} \in \RR \circ \RR^{-1}$.
But $\RR$ is many-to-one. 
This means that:
:$\forall x \in S: \tuple {x, y_1} \in \RR \land \tuple {x, y_2} \in \RR \implies y_1 = y_2$
So:
Thus (trivially) $\RR \circ \RR^{-1}$ is transitive.
Category:Composite Relations
Category:Transitive Relations
Many-to-One Relation Extends to Mapping

== Theorem ==
Let $S$ and $T$ be sets.
Let $T$ be non-empty.
Let $\RR \subset S \times T$ be a many-to-one relation.
Then there exists a mapping $f: S \to T$ such that $\RR \subseteq f$.
== Proof ==
Since $T$ is not empty, it has an element $t_0$.
Define a mapping $g: S \setminus \Preimg \RR$ by letting $\map g x = t_0$ for all $x \in S$.
Let $f = \RR \cup g$ be a relation on $S \times T$.
By Union of Many-to-One Relations with Disjoint Domains is Many-to-One, $f$ is a many-to-one relation.
By Union with Relative Complement, $f$ is total.
Thus $f$ is a mapping.
Category:Relation Theory
Category:Mapping Theory
Map from Set of Continuous Functions on Interval to Set of their Integrals

== Theorem ==
Let $\Bbb I = \closedint a b$ be a closed interval on the set of real numbers $\R$ such that $a < b$.
Let $A$ denote the set of all continuous real functions $f: \Bbb I \to \R$.
Let $B \subseteq A$ denote the set of all functions differentiable on $\Bbb I$ whose derivative is continuous on $\Bbb I$.
Let $C \subseteq B$ denote the subset of $B$ which consists of all elements of $B$ such that $\map f a = 0$.
For each $f \in A$, let $h$ denote the mapping defined as:
:$\map {\paren {\map h f} } x = \ds \int_a^x \map f t \rd t$
Then:
:$h: A \to C$
== Proof ==
Let $f \in A$ be an arbitrary continuous real function $f: \Bbb I \to \R$.
From Continuous Real Function is Darboux Integrable, $\map {\paren {\map h f} } x$ exists and is continuous on $\Bbb I$.
Let $x = a$.
Then we have:
Thus $h$ is a continuous real function on $\Bbb I$ such that $\map h a = 0$.
Further, by definition, $\ds \int \map f t \rd t$ is the primitive of $f$, and exists by dint of the above.
It follows from the Fundamental Theorem of Calculus that $f = \map {\dfrac \d {\d x} } h$ and so $\map h x$ is functions differentiable on $\Bbb I$.
Thus it is shown that $C \subseteq B \subseteq A$ and the result follows.
== Sources ==
* : Chapter $1$: Theory of Sets: $\S 9$: Inverse Functions, Extensions, and Restrictions: Exercise $1$ 
Category:Integral Calculus
Category:Continuous Real Functions
Mapping/Examples

== Examples of Mappings ==
=== Rotation of Cartesian Plane Anticlockwise through $30 \degrees$ ===
=== $\paren {x - 2}^2 + 1$ Mapping on $\N$ ===
=== $x^3 - x$ Mapping on $\R$ ===
=== Area and Circumference of Circle ===
=== Definite Integral ===
=== Age of a Person ===
=== Height of a Person ===
=== Birthday of a Person ===
Thus it is seen that multiple mappings may be defined on the same set.
=== Population of Nation ===
=== Stretch of Spring ===
=== Marks in an Examination ===
=== Arbitrary Sets of Students ===
== Further Examples of Relations which May or May Not be Mappings ==
=== Questionable mapping on Arbitrary Sets ===
The following examples consist of relations on the real numbers $\R$ which may or may not be mappings from $\R$ to $\R$:
=== Questionable mapping: $x^2 + y^2 = 1$ ===
=== Questionable mapping: $x y = 1$ ===
=== Questionable mapping: $x^4 + y^3 = 1$ ===
=== Questionable mapping: $x^3 + y^4 = 1$ ===
=== Questionable mapping: $\sqrt x + \sqrt y = 1$ ===
== Sources ==
* : $\S 3.1$. Mappings: Example $44$
Category:Examples of Mappings
Mapping/Examples/(x-2)^2+1 on Natural Numbers

== Example of Mapping which is neither Injective nor Surjective==
Let $f: \N \to \N$ be the mapping defined on the set of natural numbers as:
:$\forall x \in \N: \map f x = \paren {x - 2}^2 + 1$
Then $f$ has an infinite image set, but is neither a surjection nor an injection.
== Proof ==
We have that:
:$17 = \paren {6 - 2}^2 + 1$
and so $17 = \map f 6$.
That is:
:$17 \in \Img f$
Let $y \in \Img f$ such that $y \ge 17$.
Then:
:$\exists x \in \N: y = \map f x = \paren {x - 2}^2 + 1$
such that $x > 6$.
Now consider:
That is for every $y \in \Img f$ such that $y \ge 17$, there exists $y' \in \Img f$ such that $y' > 5$.
Thus $f$ is unbounded above.
It follows that $\Img f$ is an infinite set.
For all $x \in \N$ we have that $\paren {x - 2}^2 \ge 0$.
Thus:
:$\paren {x - 2}^2 + 1 \ge 1$
Consider the natural number $y = 0$.
Then there exists no $x \in \N$ such that $\map f x = y$.
Thus, by definition, $f$ is not a surjection.
Let $x_1 = -2, x_2 = 6$.
Then:
while:
Thus we have found $x_1, x_2 \in \Dom f$ such that $x_1 \ne x_2$ but that $\map f {x_1} = \map f {x_2}$.
Thus:
Thus by definition $f$ is not an injection.
== Sources ==
* : Chapter $4$: Mappings: Exercise $5 \ \text{(a)}$
Category:Examples of Mappings
Mapping/Examples/Age of Person

== Example of Mapping ==
Let $P$ be the set of all people.
Let $\theta: P \to \Z$ be the mapping defined as:
:$\forall x \in P: \map \theta x = \text { the age of $x$ last birthday}$
== Sources ==
* : $\S 3.1$. Mappings: Example $43$
Category:Examples of Mappings
Mapping/Examples/Arbitrary Sets

== Example of Relation which is not a Mapping ==
Let $A = \set {a, b, c}$.
Let $B = \set {1, 2, 3, 4}$.
Let $g_1 \subseteq {A \times B}$ such that:
:$g_1 = \set {\tuple {a, 2}, \tuple {b, 4} }$
Let $g_2 \subseteq {A \times B}$ such that:
:$g_2 = \set {\tuple {a, 3}, \tuple {b, 1}, \tuple {c, 2}, \tuple {c, 4} }$
Let $g_3 \subseteq {A \times B}$ such that:
:$g_3 = \set {\tuple {a, 4}, \tuple {b, 4}, \tuple {c, 2} }$
Then $g_3$ is a mapping.
However, neither $g_1$ nor $g_2$ is a mapping.
== Proof ==
We have that:
:$\forall x \in A: \exists \tuple {x, y} \in g_3$
:$\forall x \in A: \exists \tuple {x, y_1} \in g_3 \land \tuple {x, y_2} \in g_3 \implies y_1 = y_2$
and so $g_3$ is indeed a mapping.
We have:
:$\nexists \tuple {x, y} \in g_1: x = c$
so $g_1$ is not a mapping.
We have:
:$\tuple {c, 2} \in g_2$ and $\tuple {c, 4} \in g_2$
but:
:$2 \ne 4$
and so $g_2$ is not a mapping.
== Sources ==
* : Appendix $\text{A}.4$: Functions
Category:Examples of Mappings
Mapping/Examples/Area and Circumference of Circle

== Examples of Mappings ==
Let $A$ denote the set of circles.
Let $f_1: A \to \R$ be the mapping defined on $A$ as:
:$\forall a \in A: \map {f_1} a = \map {\Area} a$
Let $f_2: A \to \R$ be the mapping defined on $A$ as:
:$\forall a \in A: \map {f_2} a = \map {\operatorname {Circ} } a$
where $\map {\operatorname {Circ} } a$ denotes the circumference of $a$.
== Sources ==
* : Appendix $\text{A}.4$: Functions
Category:Examples of Mappings
Mapping/Examples/Birthday of Person

== Example of Mapping ==
Let $P$ be the set of all people.
Let $S$ be the set of all dates in the calendar.
Let $\chi: P \to S$ be the mapping defined as:
:$\forall x \in P: \map \chi x = \text { the birthday of $x$}$
== Sources ==
* 
* 
Category:Examples of Mappings
Mapping/Examples/Definite Integral

== Example of Mapping ==
Let $\mathscr C$ be the set of continuous real functions defined on a closed interval $\closedint a b$.
The definite integral is a mapping which associates an element $f \in \mathscr C$ with a real number $\ds \int_a^b \map f x \rd x$.
== Sources ==
* : Chapter $1$: Theory of Sets: $\S 6$: Functions
Category:Examples of Mappings
Mapping/Examples/Height of Person

== Example of Mapping ==
Let $P$ be the set of all people.
Let $\theta: P \to \Z$ be the mapping defined as:
:$\forall x \in P: \map \phi x = \text { the height of $x$ in mm}$
== Sources ==
* : $\S 3.1$. Mappings: Example $44$
Category:Examples of Mappings
Mapping/Examples/Population of Nation

== Example of Mapping ==
Let $T$ be the set of all times.
Let $N$ be a nation in the world.
Let $P: T \to \N$ be the mapping defined as:
:$\forall t \in T: \map P t = \text {the population of $N$ at time $t$}$
== Sources ==
* : Chapter $1$: Functions: Example 1
Category:Examples of Mappings
Mapping/Examples/Rotation through 30 Degrees

== Example of Mapping ==
Let $\Gamma$ be the Cartesian plane.
The rotation $R_{30 \degrees}$ of $\Gamma$ anticlockwise through an angle of $30 \degrees$ about the origin $O$ is a mapping from $\Gamma$ to $\Gamma$.
== Proof ==
For every point $P$ in $\Gamma$ which is not the origin $O$ it is possible to:
:construct a straight line $OP$
:construct a straight line $OP'$ at an angle of $30 \degrees$ to $OP$ measured in an anticlockwise direction
:construct the point $P'$ such that $\len \paren {OP} = \len \paren {OP'}$.
:
It can be seen that for every $P$ there is a unique $P'$ to which $R_{30 \degrees}$ maps $P$, apart from $O$ which is mapped to $O$.
== Sources ==
* : $\S 20 \ (2)$: Introduction
Category:Examples of Mappings
Mapping/Examples/Stretch of Spring

== Example of Mapping ==
Let $S$ be a spring.
Let $W$ be a weight placed on the end of $S$.
Let $G: \R \to \R$ be the mapping defined as:
:$\map G W = \text {the stretch of $S$ under $W$}$
== Sources ==
* : Chapter $1$: Functions: Example 2
Category:Examples of Mappings
Mapping/Examples/root x + root y = 1

== Example of Relation which is not a Mapping ==
Let $R_5$ be the relation defined on the Cartesian plane $\R \times \R$ as:
:$R_5 = \set {\tuple {x, y} \in \R \times \R: \sqrt x + \sqrt y = 1}$
Then $R_5$ is not a mapping.
== Proof ==
$R_5$ fails to be a mapping because, for example, $\sqrt x$ does not exist for $x < 0$.
Thus $R_5$ is undefined for $x <0$.
Thus $R_5$ fails to be left-total.
We have:
== Sources ==
* : Chapter $1$: Mappings: $\S 10 \alpha$
Category:Examples of Mappings
Mapping/Examples/x^2 + y^2 = 1

== Example of Relations which is not a Mapping ==
Let $R_1$ be the relation defined on the Cartesian plane $\R \times \R$ as:
:$R_1 = \set {\tuple {x, y} \in \R \times \R: x^2 + y^2 = 1}$
Then $R_1$ is not a mapping.
== Proof ==
$R_1$ fails to be a mapping for the following reasons:
$(1): \quad$ For $x < -1$ and $x > 1$, there exists no $y \in \R$ such that $x^2 + y^2 = 1$.
Thus $R_1$ fails to be left-total.
$(2): \quad$ For $-1 < x < 1$, there exist exactly two $y \in \R$ such that $x^2 + y^2 = 1$, for example:
So both $\tuple {\dfrac 1 2, \dfrac {\sqrt 3} 2}$ and $\tuple {\dfrac 1 2, -\dfrac {\sqrt 3} 2}$ are elements of $R_1$.
Thus $R_1$ fails to be many-to-one.
== Sources ==
* : Chapter $1$: Mappings: $\S 10 \alpha$
Category:Examples of Mappings
Mapping/Examples/x^3-x on Real Numbers

== Example of Mapping ==
Let $f: \R \to \R$ be the mapping defined on the set of real numbers as:
:$\forall x \in \R: \map f x = x^3 - x$
Then $f$ is a surjection but not an injection.
== Proof ==
Let $y \in \R$.
As $x \to \infty$, we have that $y \to \infty$.
Similarly, as $x \to -\infty$, we have that $y \to -\infty$.
From Real Polynomial Function is Continuous, $f$ is continuous on $\R$.
It follows from the Intermediate Value Theorem that:
:$\forall y \in \R: \exists x \in \R: y = \map f x$
Thus, by definition, $f$ is a surjection.
We have that:
demonstrating that $f$ is not an injection.
== Sources ==
* : Appendix $\text{A}.4$: Functions: Problem Set $\text{A}.4$: $22$
* : Chapter $2$: Maps and relations on sets: Example $2.5$
Category:Examples of Mappings
Category:Examples of Surjections
Category:Examples of Injections
Mapping/Examples/x^3 + y^4 = 1

== Example of Relation which is not a Mapping ==
Let $R_4$ be the relation defined on the Cartesian plane $\R \times \R$ as:
:$R_4 = \set {\tuple {x, y} \in \R \times \R: x^3 + y^4 = 1}$
Then $R_4$ is not a mapping.
== Proof ==
$R_4$ fails to be a mapping for the following reasons:
$(1): \quad$ For $x > 1$, there exists no $y \in \R$ such that $x^3 + y^4 = 1$.
Thus $R_4$ fails to be left-total.
$(2): \quad$ For $x < 1$, there exist exactly two $y \in \R$ such that $x^3 + y^4 = 1$, for example:
So both $\tuple {0, 1}$ and $\tuple {0, -1}$ are elements of $R_4$.
Thus $R_4$ fails to be many-to-one.
== Sources ==
* : Chapter $1$: Mappings: $\S 10 \alpha$
Category:Examples of Mappings
Mapping/Examples/x^4 + y^3 = 1

== Example of Mapping ==
Let $R_3$ be the relation defined on the Cartesian plane $\R \times \R$ as:
:$R_3 = \set {\tuple {x, y} \in \R \times \R: x^4 + y^3 = 1}$
Then $R_3$ is a mapping.
== Proof ==
We have that:
:$\forall x \in \R: \exists! y \in \R: \sqrt [3] {1 - x^4}$
and so $R_3$ is both left-total and many-to-one.
== Sources ==
* : Chapter $1$: Mappings: $\S 10 \alpha$
Category:Examples of Mappings
Mapping/Examples/x y = 1

== Example of Relation which is not a Mapping ==
Let $R_2$ be the relation defined on the Cartesian plane $\R \times \R$ as:
:$R_2 = \set {\tuple {x, y} \in \R \times \R: x y = 1}$
Then $R_2$ is not a mapping.
== Proof ==
$R_2$ fails to be a mapping for the following reason:
For $x = 0$, there exists no $y \in \R$ such that $x y = 1$.
Thus $R_2$ fails to be left-total.
== Sources ==
* : Chapter $1$: Mappings: $\S 10 \alpha$
Category:Examples of Mappings
Mapping/Mistakes/Image Element Multiply Defined

== Example of Mistake in Definition of Mapping ==
This example of an attempted definition of a mapping contains a mistake.
:$h: \R \to \R$ defined as: $\forall x \in \R: x \mapsto \begin{cases} x + 1 & : x \ge 0 \\ 0 & : x \le 0 \end{cases}$
== Explanation ==
The element $0 \in \Dom h$ is defined twice:
:$h \paren 0 = 0 + 1 = 1$
and:
:$h \paren 0 = 0$
== Sources ==
* : Chapter $4$: Mappings: Exercise $1 \ \text {(iii)}$
Category:Examples of Mistakes in Mapping Definitions
Category:Mistakes
Mapping/Mistakes/Image Element Undefined

== Example of Mistake in Definition of Mapping ==
This example of an attempted definition of a mapping contains a mistake.
:$g: \R \to \R$ defined as: $\forall x \in \R: x \mapsto \dfrac 1 x$
== Explanation ==
The image of the element $0 \in \R$ is undefined:
:$g \paren 0 = \dfrac 1 0$
== Sources ==
* : Chapter $4$: Mappings: Exercise $1 \ \text {(ii)}$
Category:Examples of Mistakes in Mapping Definitions
Category:Mistakes
Mapping/Mistakes/Image Elements not in Codomain

== Example of Mistake in Definition of Mapping ==
This example of an attempted definition of a mapping contains a mistake.
:$f: \N \to \N$ defined as: $\forall x \in \N: x \mapsto x - 7$
== Explanation ==
The codomain of $f$ is:
:$\Cdm f = \set {0, 1, 2, \ldots}$
However, consider the subset $S \subset \Dom f$ of the domain of $f$ where $S = \set {0, 1, 2, 3, 4, 5, 6}$:
:$f \sqbrk S = \set {-7, -6, -5, -4, -3, -2, -1}$
and none of the elements of the image of $S$ are actually elements of $\Cdm f$.
That is:
:$\Img f \nsubseteq \Cdm f$
== Sources ==
* : Chapter $4$: Mappings: Exercise $1 \ \text {(i)}$
Category:Examples of Mistakes in Mapping Definitions
Category:Mistakes
Mapping/Mistakes/Mapping not Well-Defined

== Example of Mistake in Definition of Mapping ==
This example of an attempted definition of a mapping contains a mistake.
:$\theta: \Q \to \Z$ defined as: $\forall m, n \in \Z, n \ne 0: \dfrac m n \mapsto m + n$
== Explanation ==
The mapping $\theta$ is not well-defined.
Let $x \in \Q$ be such that $x = \dfrac 1 2$.
Then:
:$\theta \paren {\dfrac 1 2} = 1 + 2 = 3$
:$\theta \paren {\dfrac 2 4} = 2 + 4 = 6$
:$\theta \paren {\dfrac 3 6} = 3 + 6 = 9$
and so on.
Thus $\theta \paren {\dfrac 1 2} = \set {3, 6, 9, \ldots}$
If $\theta$ were to be defined as:
:$\theta: \Z \times \Z: \tuple {m, n} \mapsto m + n$
that would be valid.
However, the fact that each of $\dfrac 1 2, \dfrac 2 4, \dfrac 3 6, \ldots$ all refer to the same $x \in \Q$ renders $\theta$ as not actually a mapping.
== Sources ==
* : Chapter $4$: Mappings: Exercise $1 \ \text {(iv)}$
Category:Examples of Mistakes in Mapping Definitions
Category:Mistakes
Mapping Assigning to Element Its Compact Closure is Order Isomorphism

== Theorem ==
Let $L = \struct {S, \vee, \preceq}$ be a bounded below algebraic join semilattice.
Let $C = \struct {\map K L, \preceq'}$ be an ordered subset of $L$
where $\map K L$ denotes the compact subset of $L$.
Let $I = \struct {\map {\mathit {Ids} } C, \precsim}$ be an inclusion ordered set
where $\map {\mathit {Ids} } C$ denotes the set of all ideals in $C$.
Let $f: S \to \map {\mathit {Ids} } C$ be a mapping such that
:$\forall x \in S: \map f x = x^{\mathrm {compact} }$
where $x^{\mathrm {compact} }$ denotes the compact closure of $x$.
Thus $f$ is order isomorphism between $L$ and $I$.
== Proof ==
We will prove that
:$f$ is an order embedding.
Let $x, y \in S$.
Sufficient condition
Assume that
:$x \preceq y$
By Compact Closure is Increasing:
:$x^{\mathrm {compact} } \subseteq y^{\mathrm {compact} }$
By definition of $f$:
:$\map f x \subseteq \map f y$
Thus by definition of inclusion ordered set:
:$\map f x \precsim \map f y$
Necessary condition
Assume that:
:$\map f x \precsim \map f y$
By definition of inclusion ordered set:
:$\map f x \subseteq \map f y$
By definition of $f$:
:$x^{\mathrm {compact} } \subseteq y^{\mathrm{compact} }$
By Supremum of Subset:
:$\map \sup {x^{\mathrm {compact} } } \preceq \map \sup {y^{\mathrm {compact} } }$
By definition of algebraic:
:$L$ satisfies the axiom of $K$-approximation.
Thus by the axiom of $K$-approximation:
:$x \preceq y$
We will prove that
:$f$ is a surjection.
Let $y \in \map {\mathit {Ids} } C$
Define $x = \sup_L y$
Thus $x \in S$.
We will prove that:
:$x^{\mathrm {compact} } \subseteq y$
Let $d \in x^{\mathrm {compact} }$
By definition of compact closure:
:$d$ is a compact element and $d \preceq x$
By definition of compact subset:
:$d \in \map K L$
By definition of compact element:
:$d \ll d$
where $\ll$ denotes the way below relation.
By definition of way below relation:
:$\exists z \in y: d \preceq z$
By definition of ordered subset:
:$d \preceq' z$
Thus by definition of lower section:
:$d \in y$
We will prove that
:$y \subseteq x^{\mathrm {compact} }$
Let $d \in y$.
By definition of subset:
:$d \in \map K L$
By definition of compact subset:
:$d$ is a compact element.
By definition of supremum:
:$x$ is upper bound for $y$.
By definition of upper bound:
:$d \preceq x$
Thus by definition of compact closure:
:$d \in x^{\mathrm {compact} }$
By definition of set equality:
:$y = x^{\mathrm {compact} }$
Hence:
:$y = \map f x$
Hence $f$ is order isomorphism.
== Sources ==
* 
* 
Category:Order Isomorphisms
Mapping Assigning to Element Its Lower Closure is Isomorphism

== Theorem ==
Let $L = \struct {S, \vee, \preceq}$ be a bounded below join semilattice.
Let $I = \struct {\map {\mathit {Ids} } L, \precsim}$ be an inclusion ordered set
where:
:$\map {\mathit {Ids} } L$ denotes the set of all ideals in $L$
:$\mathord \precsim = \mathord \subseteq \cap \paren {\map {\mathit {Ids} } L \times \map {\mathit {Ids} } L}$
Let $P = \struct {\map K I, \precsim'}$ be an ordered subset of $I$
where:
:$\map K I$ denotes the compact subset of $I$.
Let $f: S \to \map K I$ be a mapping such that:
:$\forall x \in S: \map f x = x^\preceq$
Then $f$ is an order isomorphism between $L$ and $P$.
== Proof ==
By definition:
:$\forall x \in S: x^\preceq$ is a principal ideal.
By Compact Element iff Principal Ideal:
:$\forall x \in S: x^\preceq$ is a compact element in $I$.
By definition of compact subset:
:$\forall x \in S: x^\preceq \in \map K I$
Then $f$ is well-defined.
We will prove that:
:$f$ is an order embedding.
That means:
:$\forall x, y \in S: x \preceq y \iff \map f x \precsim' \map f y$
Let $x, y \in S$.
We will prove as lemma that:
:$x^\preceq \subseteq y^\preceq \implies x \preceq y$
Assume that:
:$x^\preceq \subseteq y^\preceq$
By definition of reflexivity:
:$x \preceq x$
By definition of lower closure of element:
:$x \in x^\preceq$
By definition of subset:
:$x \in y^\preceq$
Thus by definition of lower closure of element:
:$x \preceq y$
:$x \preceq y$
:
:$x^\preceq \subseteq y^\preceq$ by lemma and Lower Closure is Increasing
:
:$\map f x \subseteq \map f y$ by definition of $f$
:
:$\map f x \precsim \map f y$ by definition of $\precsim$
:
:$\map f x \precsim' \map f y$ by definition of ordered subset.
We will prove that:
:$\forall a \in \map K I: \exists y \in S: a = \map f y$
Let $a \in \map K I$.
By definition of compact subset:
:$a$ is a compact element in $I$.
By Compact Element iff Principal Ideal:
:$a$ is a principal ideal.
By definition of principal ideal:
:$\exists y \in S: a = y^\preceq$
Thus by definition of $f$:
:$a = \map f y$
Thus $f$ is a surjection.
Hence $f$ is an order isomorphism.
== Sources ==
* 
* 
Category:Join and Meet Semilattices
Category:Order Isomorphisms
Mapping Composed with Bijection forming Bijection is Bijection

== Theorem ==
Let $A$, $B$ and $C$ be sets.
Let $f: A \to B$ and $g: B \to C$ be mappings.
Let the composite mapping $g \circ f$ be a bijection.
Let either $f$ or $g$ be a bijection.
Then both $f$ and $g$ are bijections.
== Proof ==
We note that $g \circ f$ is both an injection and a surjection by definition of bijection.
We are given that:
:$g \circ f$ is a bijection.
From Injection if Composite is Injection it follows that $f$ is an injection.
From Surjection if Composite is Surjection it follows that $g$ is a surjection.
First suppose that $g$ is a bijection.
We already have that $f$ is an injection.
 $f$ is not a surjection.
Then:
:$\exists y \in B: \neg \exists x \in A: \map f x = y$
But then $g$ is a surjection and so:
:$\forall z \in C: \exists y \in B: z = \map g y$
and so:
:$\exists z \in C: \neg \exists x \in A: \map g {\map f x} = z$
and so $g \circ f$ is not a surjection.
This contradicts our assertion that $g \circ f$ is a bijection and so a surjection.
Hence by Proof by Contradiction $f$ must be a surjection
So $f$ is both an injection and a surjection, and so a bijection.
Now suppose that $f$ is a bijection.
 $g$ is not an injection.
Then:
:$\exists y_1, y_2 \in B: \map g {y_1} = \map g {y_2}$
But then $f$ is a bijection and so:
:$\exists x_1, x_2 \in A: y_1 = \map f {x_1} \ne \map f {x_2} = y_2$
and so:
:$\exists x_1, x_2 \in A: \map g {\map f {x_1} } = \map g {\map f {x_2} }$
and so $g \circ f$ is not an injection.
This contradicts our assertion that $g \circ f$ is a bijection and so an injection.
Hence by Proof by Contradiction $g$ must be an injection.
So $g$ is both an injection and a surjection, and so a bijection.
Hence the result.
Category:Bijections
Category:Composite Mappings