nyuuzyou/wikis huggingface dataset:
Included Set Topology on Union

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space on a set $S$.
Let $\family {A_i}_{i \mathop \in I}$ be a family of subsets of $S$ indexed by the indexing set $I$:
:$\forall i \in I: A_i \subseteq S$
Let $\forall i \in I: \map T {A_i} = \struct {S, \tau_{A_i} }$ be the included set spaces on $S$ by $A_i$.
Let:
:$\forall i \in I: \map T {A_i} \ge T$
where $\map T {A_i} \ge T$ denotes that $\map T {A_i}$ is finer than $T$.
Then:
:$\ds \map T {\bigcup A_i} \ge T$
where $\ds \map T {\bigcup A_i}$ is the included set space on $S$ by $\ds \bigcup_{i \mathop \in I} A_i$.
== Proof ==
For ease of notation, define:
:$A := \ds \bigcup_{i \mathop \in I} A_i$
and let $\tau_A$ denote the included set topology on $S$ by $A$.
Let $U \in \tau$ be nonempty.
As $\map T {A_i}$ is finer than $T$ it follows by definition that:
:$\forall i \in I: \tau \subseteq \tau_{A_i}$
Thus:
:$\forall i \in I: U \in \tau_{A_i}$
Hence for all $i$ there is a subset $Z_i \subseteq S$ of $S$, such that $U = A_i \cup Z_i$; that is:
:$\ds U = \bigcup_{i \mathop \in I} \paren {A_i \cup Z_i} = \paren {\bigcup_{i \mathop \in I} A_i} \cup \paren {\bigcup_{i \mathop \in I} Z_i}$
where the latter equality follows from associativity and commutativity of set union.
That is:
:$U = A \cup Z$
where:
:$\ds Z = \paren {\bigcup_{i \mathop \in I} Z_i}$
Hence $U \in \tau_A$. by definition of the included set topology.
This comes down to $\tau \subseteq \tau_A$, and hence $\ds \map T {\bigcup A_i} \ge T$, by definition of a finer topology.
== Sources ==
* : Chapter $\text {I}$: Topological Spaces: $1$. Open Sets and Closed Sets: Exercise $1 \ \text{(c)}$
Category:Included Set Topology
Inclusion-Exclusion Principle/Corollary

== Corollary to Inclusion-Exclusion Principle ==
Let $\SS$ be an algebra of sets.
Let $A_1, A_2, \ldots, A_n$ be finite sets which are pairwise disjoint.
Let $f: \SS \to \R$ be an additive function.
Then:
:$\ds \map f {\bigcup_{i \mathop = 1}^n A_i} = \sum_{i \mathop = 1}^n \map f {A_i}$
== Proof ==
As $A_1, A_2, \ldots, A_n$ are pairwise disjoint, their intersections are all empty.
Then Inclusion-Exclusion Principle holds.
However, from Cardinality of Empty Set, all the terms apart from the first vanish.
== Comment ==
This result is usually quoted in the context of combinatorics, where $f$ is the cardinality function.
It is also seen in the context of probability theory, in which $f$ is taken to be a probability measure.
Category:Set Systems
Category:Set Union
Category:Probability Theory
Category:Combinatorics
Inclusion-Exclusion Principle/Examples/3 Events in Event Space

== Examples of Use of Inclusion-Exclusion Principle ==
Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space.
Let $A, B, C \in \Sigma$.
Then:
== Proof ==
The Inclusion-Exclusion Principle is applicable for an additive function on an algebra of sets.
We have that $\Sigma$ is a $\sigma$-algebra.
Hence by definition, $\Sigma$ is an algebra of sets which is closed under countable unions.
Hence, a fortiori, $\Sigma$ is an algebra of sets.
We have by definition of probability measure, that $\Pr$ is an additive function fulfilling certain conditions.
The result then follows as a special case of the Inclusion-Exclusion Principle.
== Sources ==
* : $1$: Events and probabilities: $1.4$: Probability spaces: Exercise $8$
Category:Inclusion-Exclusion Principle
Inclusion-Exclusion Principle/Examples/3 Events in Event Space: Example

== Examples of Use of Inclusion-Exclusion Principle ==
Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space.
Let $A, B, C \in \Sigma$ such that:.
Then:
The probability that exactly $2$ of the events $A$, $B$ and $C$ occur is $\dfrac 6 {10}$.
== Proof ==
We are looking for the probability of:
:$\paren {\paren {A \cap B} \setminus \paren {A \cap B \cap C} } \cup \paren {\paren {B \cap C} \setminus \paren {A \cap B \cap C} } \cup \paren {\paren {A \cap C} \setminus\paren {A \cap B \cap C} }$
We have that:
:$\paren {\paren {A \cap B} \setminus \paren {A \cap B \cap C} } \cap \paren {A \cap B \cap C} = \O$
and similarly for the other two such terms.
Then we have that $\paren {A \cap B} \setminus \paren {A \cap B \cap C}$, $\paren {\paren {B \cap C} \setminus \paren {A \cap B \cap C} }$ and $\paren {\paren {A \cap C} \setminus \paren {A \cap B \cap C} }$ are pairwise disjoint.
Hence the probability $P$ that exactly $2$ of the events $A$, $B$ and $C$ occur is
== Sources ==
* : $1$: Events and probabilities: $1.4$: Probability spaces: Exercise $9$
Category:Inclusion-Exclusion Principle
Inclusion Functor is Functor

== Theorem ==
Let $\mathbf D$ be a metacategory, and let $\mathbf C$ be a subcategory of $\mathbf D$.
Let $\Iota_{\mathbf C}: \mathbf C \to \mathbf D$ be the inclusion functor on $\mathbf C$
Then:
:$\Iota_{\mathbf C}$ is a (covariant) functor
== Proof ==
Let $f, g$ be morphisms of $\mathbf C$ such that $g \circ f$ is defined.
Then:
Also, for any object $C$ of $\mathbf C$:
Hence $\Iota_{\mathbf C}$ is shown to be a covariant functor.
== Sources ==
* : Chapter $\text I$ Categories, Functors and Natural Transformations: $\S \text{3}$ Functors
Category:Functors
Inclusion Mapping is Continuous

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space.
Let $T_H = \struct {H, \tau_H}$ be a topological subspace of $T$ where $H \subseteq S$.
Let $i_H: H \to S$ be the inclusion mapping on $H$.
Then $i_H$ is a $\struct {\tau_H, \tau}$-continuous mapping.
== Proof 1 ==
== Proof 2 ==
Category:Inclusion Mapping is Continuous
Inclusion Mapping is Continuous/Proof 1

== Theorem ==
== Proof ==
From Topological Subspace is Topological Space, $\struct {H, \tau_H}$ is a topological space.
Let $U \in \tau$.
Then from Preimage of Subset under Inclusion Mapping:
:$\map {i_H^{-1} } U = U \cap H$
From the definition of the subspace topology:
:$U \cap H \in \tau_H$
Hence the result by definition of a continuous mapping.
Category:Inclusion Mapping is Continuous
Inclusion Mapping is Continuous/Proof 2

== Theorem ==
== Proof ==
Let $1_H$ be the identity mapping on $H$.
From Continuity of Composite with Inclusion: Inclusion on Mapping, $1_H$ is $\tuple {\tau_H , \tau_H}$-continuous $i_H \circ 1_H$ is $\tuple {\tau_H , \tau}$-continuous.
From Identity Mapping is Right Identity, it follows that:
:$i_H \circ 1_H = i_H$
Therefore, $1_H$ is $\tuple {\tau_H , \tau_H}$-continuous $i_H$ is $\tuple {\tau_H , \tau}$-continuous.
Because of Identity Mapping is Continuous, it follows that $i_H$ is $\tuple {\tau_H , \tau}$-continuous.
== Sources ==
* : $\S 3$: New Spaces From Old: Subspaces
Category:Inclusion Mapping is Continuous
Inclusion Mapping is Embedding

== Theorem ==
Let $T = \struct{S, \tau}$ be a topological space.
Let $T_H = \struct{H, \tau_H}$ be a topological subspace of $T$, where $H \subseteq S$.
Let $i_H : H \to S$ be the inclusion mapping of $H$ into $S$.
Then $i_H$ is a embedding of $T_H$ into $T$.
== Proof ==
== Sources ==
* : $\S 3$: New Spaces From Old: Subspaces. Topological Embeddings
Category:Topological Subspaces
Category:Embeddings (Topology)
Inclusion Mapping is Injection

== Theorem ==
Let $S, T$ be sets such that $S$ is a subset of $T$.
Then the inclusion mapping $i_S: S \to T$ defined as:
:$\forall x \in S: \map {i_S} x = x$
is an injection.
For this reason the inclusion mapping can be known as the canonical injection of $S$ to $T$.
== Proof ==
Suppose $\map {i_S} {s_1} = \map {i_S} {s_2}$.
Thus $i_S$ is an injection by definition.
== Sources ==
* : $\S 8$: Functions
* : $\S 5$. Induced mappings; composition; injections; surjections; bijections: Example $5.4$
* : Chapter $1$: Sets and mappings: $\S 1.3$: Mappings
Category:Injections
Category:Inclusion Mappings
Inclusion Mapping is Monomorphism

== Theorem ==
Let $\struct {S, \circ}$ be an algebraic structure.
Let $\struct {T, \circ}$ be an algebraic substructure of $S$.
Let $\iota: T \to S$ be the inclusion mapping from $T$ to $S$.
Then $\iota$ is a monomorphism.
== Proof ==
We have that the inclusion mapping is an injection.
Now let $x, y \in T$:
demonstrating that $\iota$ has the morphism property.
So $\iota$ is a homomorphism which is also an injection.
Thus by definition, $\iota$ is a monomorphism.
Category:Monomorphisms (Abstract Algebra)
Category:Inclusion Mappings
Inclusion Mapping is Order Embedding

== Theorem ==
Let $\struct {S, \preccurlyeq_S}$ and $\struct {T, \preccurlyeq_T}$ be ordered sets such that $S \subseteq T$.
Let ${\preccurlyeq_S} = {\preccurlyeq_T} {\restriction_S}$ be the restriction of $\preccurlyeq_T$ to $S$.
Let $i_S: S \to T$ denote the inclusion mapping from $S$ to $T$:
:$\forall s \in S: \map {i_S} s = s$
Then $i_S$ is an order embedding.
== Proof ==
We have that Inclusion Mapping is Restriction of Identity.
Then we have that Identity Mapping is Order Isomorphism.
The result follows.
== Sources ==
* : Part $1$: Not Entirely Naive Set Theory: Chapter $2$: Partial Order Relations
Category:Examples of Order Embeddings
Inclusion Mapping is Restriction of Identity

== Theorem ==
Let $T$ be a set.
Let $S \subseteq T$ be a subset of $T$.
Let $i_S: S \to T$ be the inclusion mapping on $S$.
Then $i_S$ is the restriction of the identity mapping $I_T: T \to T$ on $T$.
== Proof ==
By definition of inclusion mapping:
:$i_S: S \to T: \forall x \in S: \map {i_S} x = x$
By definition of identity mapping:
:$I_T: T \to T: \forall x \in T: \map {I_T} x = x$
The result follows by definition of restriction of mapping.
== Sources ==
* : $0$: Some Conventions and some Basic Facts
* : Chapter $1$: Sets and mappings: $\S 1.3$: Mappings
Category:Inclusion Mappings
Category:Identity Mappings
Inclusion Mapping is Surjection iff Identity

== Theorem ==
Let $T$ be a set.
Let $S\subseteq T$ be a subset.
Let $i_S: S \to T$ be the inclusion mapping.
Then:
:$i_S: S \to T$ is surjective $i_S: S \to T = I_S: S \to S$
where $I_S: S \to S$ denotes the identity mapping on $S$.
Alternatively, this theorem can be worded as:
:$i_S: S \to S = I_S: S \to S$
It follows directly that from Surjection by Restriction of Codomain‎, the surjective restriction of $i_S: S \to T$ to $i_S: S \to \Img {i_S}$ is itself the identity mapping.
== Proof ==
It is apparent from the definitions of both the inclusion mapping and the identity mapping that:
:$(1): \quad \Dom {i_S} = S = \Dom {I_S}$
:$(2): \quad \forall s \in S: \map {i_S} s = s = \map {I_S} s$
=== Necessary Condition ===
Let $i_S: S \to T = I_S: S \to S$.
From Equality of Mappings, we have that the codomain of $i_S$ equals the codomain of $I_S$.
Thus the codomain of $i_S$ equals the codomain of $I_S$ equals $S$ and thus $T = S$.
So $\forall s \in S: s = \map {i_S} s$ and so $i_S$ is surjective.
=== Sufficient Condition ===
Now let $i_S: S \to T$ be a surjection.
Then:
:$\forall s \in T: s = \map {i_S} s \implies s \in S$
and therefore:
:$T \subseteq S$
Thus:
:$T = S$
and so the codomain of $i_S$ equals the codomain of $I_S$ which equals $S$.
Thus $i_S: S \to T = I_S: S \to S$.
== Sources ==
* : $\S 8$: Functions
Category:Surjections
Category:Inclusion Mappings
Category:Identity Mappings
Inclusion Mapping on Metric Space is Continuous

== Theorem ==
Let $M = \struct {A, d}$ be a metric space.
Let $\struct {H, d_H}$ be a metric subspace of $M$.
Then the inclusion mapping $i_H: H \to A$ is continuous from $\struct {H, d_H}$ to $\struct {A, d}$.
== Proof ==
Let $a \in H$.
Let $\epsilon \in \R_{>0}$.
Let $\delta = \epsilon$.
Then:
So by definition $i_H$ is continuous at $a$ $d_H$ and $d$.
As $a \in H$ is arbitrary, it follows that $i_H$ is continuous from $\struct {H, d_H}$ to $\struct {A, d}$.
== Sources ==
* : Chapter $2$: Metric Spaces: $\S 7$: Subspaces and Equivalence of Metric Spaces: Theorem $7.2$
Category:Inclusion Mappings
Category:Metric Subspaces
Category:Continuous Mappings
Inclusion Mapping on Subgroup is Homomorphism

== Theorem ==
Let $\struct {G, \circ}$ be a group.
Let $\struct {H, \circ_{\restriction H} }$ be a subgroup of $G$.
Let $i: H \to G$ be the inclusion mapping from $H$ to $G$.
Then $i$ is a group homomorphism.
== Proof ==
Let $x, y \in H$.
From , $x \circ_{\restriction H} y \in H$.
Then:
Hence the result by definition of group homomorphism.
== Sources ==
* : Chapter $\text{II}$: Groups: Morphisms
Category:Group Homomorphisms
Category:Inclusion Mappings
Inclusion Mapping on Subgroup is Monomorphism

== Theorem ==
Let $\struct {G, \circ}$ be a group.
Let $\struct {H, \circ {\restriction_H} }$ be a subgroup of $G$.
Let $i: H \to G$ be the inclusion mapping from $H$ to $G$.
Then $i$ is a group monomorphism.
== Proof ==
We have:
* Inclusion Mapping on Subgroup is Homomorphism
* Inclusion Mapping is Injection
The result follows by definition of (group) monomorphism.
== Sources ==
* : Chapter $\text{II}$: Groups: Quotient Groups
Category:Group Monomorphisms
Category:Inclusion Mappings
Inclusion Mapping on Subring is Homomorphism

== Theorem ==
Let $\struct {R, +, \circ}$ be a ring.
Let $\struct {S, +{\restriction_S}, \circ {\restriction_S}}$ be a subring of $R$.
Let $i_S: S \to R$ be the inclusion mapping from $S$ to $R$.
Then ${i_S}$ is a ring homomorphism.
== Proof ==
Let $x, y \in S$.
Then:
and:
Hence ${i_S}$ is a ring homomorphism by definition.
Category:Ring Homomorphisms
Category:Inclusion Mappings
Inclusion Mapping on Subring is Monomorphism

== Theorem ==
Let $\struct {R, +, \circ}$ be a ring.
Let $\struct {S, +{\restriction_S}, \circ {\restriction_S} }$ be a subring of $R$.
Let $i_S: S \to R$ be the inclusion mapping from $S$ to $R$.
Then $i_S$ is a ring monomorphism.
== Proof ==
By Inclusion Mapping on Subring is Homomorphism, $i_S$ is a ring homomorphism.
By Inclusion Mapping is Injection, $i_S$ is an injection.
The result follows by definition of (ring) monomorphism.
Category:Group Monomorphisms
Category:Inclusion Mappings
Inclusion Mappings to Topological Sum from Components

== Theorem ==
Let $\struct {X, \tau_1}$ and $\struct {Y, \tau_2}$ be topological spaces.
Let $\struct {Z, \tau_3}$ be the topological sum of $X$ and $Y$ where $\tau_3$ is the topology generated by $\tau_1$ and $\tau_2$.
Then $\tau_3$ is the finest topology on $Z$ in which the inclusion mappings from $\struct {X, \tau_1}$ and $\struct {Y, \tau_2}$ to $\struct {Z, \tau_3}$ are continuous.
== Proof ==
== Sources ==
* : Part $\text I$: Basic Definitions: Section $1$: General Introduction: Functions
Category:Topological Sum
Category:Inclusion Mappings
Inclusion of Natural Numbers in Integers is Epimorphism

== Theorem ==
Let $\mathbf{Mon}$ be the category of monoids.
Let $\struct {\N, +}$ denote the monoid of natural numbers as on Natural Numbers under Addition form Commutative Monoid.
Let $\struct {\Z, +}$ denote the additive group of integers.
Denote with $\iota: \N \to \Z$ the inclusion mapping.
Then $\iota: \N \to \Z$ is an epimorphism in $\mathbf{Mon}$.
== Proof ==
Let $\struct {M, \circ}$ be a monoid with identity $e$.
Let $f, g: \Z \to M$ be monoid homomorphisms such that:
:$f \circ \iota = g \circ \iota$
that is, by definition of inclusion, such that:
:$\forall n \in \N: \map f n = \map g n$
Now $\iota$ will be epic if we can show that $f = g$.
The morphism property of $f$ and $g$ yields that, for any $m > 0$:
:$\map f {- m} = \map f {-1} \circ \cdots \circ \map f {-1}$
:$\map g {- m} = \map g {-1} \circ \cdots \circ \map g {-1}$
with on the $m$ copies of $\map f {-1}$ and $\map g {-1}$, respectively.
It thus is necessary and sufficient to show that $\map f {-1} = \map g {-1}$.
To this end, compute:
Hence the result.
== Caution ==
The theorem statement does not assert that $\iota$ is an abstract-algebraic epimorphism.
This is plainly false, as $\iota$ is not a surjection.
== Sources ==
* : $\S 2.1$: Example $2.5$
Category:Category of Monoids
Category:Natural Numbers
Category:Integers
Category:Inclusion Mappings
Incommensurability of Sum of Incommensurable Magnitudes

== Theorem ==
== Proof ==
Let $AB$ and $BC$ be incommensurable magnitudes which are added together to make $AC$.
Suppose $AC$ and $AB$ are not incommensurable.
Then some magnitude $D$ will measure them both.
Since $D$ measures both $AC$ and $AB$, $D$ also measures the remainder $BC$.
That is, $D$ measures $AB$ and $BC$.
Therefore from , $AB$ and $BC$ are commensurable.
But by hypothesis $AB$ and $BC$ are incommensurable.
Therefore no magnitude $D$ will measure both $AC$ and $AB$.
Therefore $AC$ and $AB$ are incommensurable.
In the same way it is shown that $AC$ and $BC$ are also incommensurable.
Now let $AC$ be incommensurable with one of either $AB$ and $BC$.
, let $AC$ be incommensurable $AB$.
Suppose $AB$ and $BC$ are not incommensurable.
Then some magnitude $D$ will measure them both.
Since $D$ measures both $AB$ and $BC$, $D$ also measures the whole $AC$.
But $D$ measures $AB$.
Therefore $D$ measures both $AC$ and $AB$.
Therefore $AC$ and $AB$ are commensurable.
But by hypothesis $AB$ and $AC$ are incommensurable.
Therefore no magnitude will measure both $AB$ and $BC$.
Therefore $AB$ and $BC$ are incommensurable.
== Sources ==
* : Book $\text{X}$. Propositions
Category:Euclidean Number Theory
Incommensurable/Examples/6 and Root 3

== Example of Incommensurability ==
$6$ and $\sqrt 3$ are incommensurable.
== Proof ==
From Square Root of Prime is Irrational, $\sqrt 3$ is irrational.
Hence the ratio $6$ to $\sqrt 3$ is irrational.
Hence the result by definition of incommensurable.
== Sources ==
* 
* 
Category:Examples of Incommensurability
Incommensurable/Examples/Root 2 and 1

== Example of Incommensurability ==
$\sqrt 2$ and $1$ are incommensurable.
== Proof ==
From Square Root of 2 is Irrational, the ratio $\sqrt 2$ to $1$ is irrational.
Hence the result by definition of incommensurable.
== Sources ==
* 
* 
Category:Examples of Incommensurability
Incommensurable Magnitudes do not Terminate in Euclid's Algorithm

== Theorem ==
== Proof ==
:
Let $AB$ and $CD$ be unequal magnitudes such that $AB < CD$ which fulfil the condition of the statement.
Suppose $AB$ and $CD$ are commensurable magnitudes.
Then by definition some magnitude will measure them both.
Let $E$ be such a magnitude that measures both $AB$ and $CD$.
Let $AB$ measure $FD$ and leave $CF$ from $CD$.
Let $CF$ measure $BG$ and leave $AG$ from $AB$.
By hypothesis, this process can be repeated indefinitely.
Let it be repeated until some magnitude be left that is less than $E$.
Since:
: $E$ measures $AB$
and:
: $AB$ measures $DF$
then:
: $E$ measures $FD$.
But $E$ also measures $CD$.
Therefore $E$ also measures $CF$.
But $CF$ measures $BG$.
Therefore $E$ also measures $BG$.
But $E$ also measures the whole of $AB$.
Therefore $E$ will also measures $AG$.
But $AG$ is less than $E$.
That means the greater magnitude measures the lesser magnitude.
From this contradiction it follows that no magnitude can measure both $AB$ and $CD$.
Therefore, by definition, $AB$ and $CD$ are incommensurable.
== Sources ==
* : Book $\text{X}$. Propositions
Category:Euclidean Number Theory
Incommensurable Magnitudes have Irrational Ratio

== Theorem ==
== Proof ==
Let $A$ and $B$ be incommensurable magnitudes.
Suppose $A$ and $B$ have the ratio which a number has to a number
Then by , $A$ and $B$ are commensurable.
From this contradiction follows the result.
== Sources ==
* : Book $\text{X}$. Propositions
Category:Euclidean Number Theory
Increasing Alternating Sum of Binomial Coefficients

== Theorem ==
Let $n \in \Z$ be an integer.
Then:
:$\ds \sum_{j \mathop = 0}^n \paren {-1}^{n + 1} j \binom n j = 0$
where $\dbinom n k$ denotes a binomial coefficient.
That is:
:$1 \dbinom n 1 - 2 \dbinom n 2 + 3 \dbinom n 3 - \cdots + \paren {-1}^{n + 1} n \dbinom n n = 0$
== Proof ==
== Sources ==
* : $\S 3$: The Binomial Formula and Binomial Coefficients: Properties of Binomial Coefficients: $3.15$
* : $\S 3$: The Binomial Formula and Binomial Coefficients: Properties of Binomial Coefficients: $3.15.$
Category:Binomial Coefficients
Increasing Mapping Preserves Lower Bounds

== Theorem ==
Let $L = \left({S, \preceq}\right)$, $L' = \left({S', \preceq'}\right)$ be ordered sets.
Let $f:S \to S'$ be an increasing mapping.
Let $x \in S$, $X \subseteq S$ such that
:$x$ is lower bound for $X$.
Then $f \left({x}\right)$ is lower bound for $f \left[{X}\right]$.
== Proof ==
Let $y \in f\left[{X}\right]$.
By definition of image of set:
:$\exists z \in X: y = f \left({z}\right)$
By definition of lower bound:
:$x \preceq z$
Thus by definition of increasing mapping:
:$f \left({x}\right) \preceq' y$
== Sources ==
* 
Category:Increasing Mappings
Increasing Mapping Preserves Upper Bounds

== Theorem ==
Let $L = \left({S, \preceq}\right)$, $L' = \left({S', \preceq'}\right)$ be ordered sets.
Let $f:S \to S'$ be an increasing mapping.
Let $x \in S$, $X \subseteq S$ such that
:$x$ is upper bound for $X$.
Then $f\left({x}\right)$ is upper bound for $f\left[{X}\right]$.
== Proof ==
Let $y \in f\left[{X}\right]$.
By definition of image of set:
:$\exists z \in X: y = f\left({z}\right)$
By definition of upper bound:
:$z \preceq x$
Thus by definition of increasing mapping:
:$y \preceq' f\left({x}\right)$
== Sources ==
* 
Category:Increasing Mappings
Increasing Mappings Satisfying Inclusion in Lower Closure is Isomorphic to Auxiliary Relations

== Theorem ==
Let $R = \struct {S, \preceq}$ be a bounded below join semilattice.
Let $\map {\operatorname{Ids} } R$ be the set of all ideals in $R$.
Let $L = \struct {\map {\operatorname{Ids} } R, \precsim}$ be an ordered set where $\precsim \mathop = \subseteq\restriction_{\map {\operatorname{Ids} } R \times \map {\operatorname{Ids} } R}$.
Let $M = \struct {F, \preccurlyeq}$ be the ordered set of increasing mappings $g:S \to \map {\operatorname{Ids} } R$ satisfying $\forall x \in S: \map g x \subseteq x^\preceq$.
Let $\map {\operatorname{Aux} } R$ be the set of all auxiliary relations on $S$.
Let $P = \struct {\map {\operatorname{Aux} } R, \precsim'}$ be an ordered set where $\precsim' \mathop = \subseteq\restriction_{\map {\operatorname{Aux} } R \times \map {\operatorname{Aux} } R}$.
Then
:there exists an order isomorphism between $P$ and $M$
== Proof ==
By Segment of Auxiliary Relation Mapping is Element of Increasing Mappings Satisfying Inclusion in Lower Closure define $G: \map {\operatorname{Aux} } R \to F$:
:$\forall \RR \in \map {\operatorname{Aux} } R: \map G \RR = \paren {S \ni x \mapsto x^\RR}$
We will prove by Order Isomorphism is Surjective Order Embedding that:
:$G$ is an order isomorphism.
=== Surjection ===
By Element of Increasing Mappings Satisfying Inclusion in Lower Closure is Generated by Auxiliary Relation:
:$\forall f \in F: \exists \RR \in \map {\operatorname{Aux} } R: f = \paren {S \ni x \mapsto x^\RR}$
By definition of image of mapping:
:$\forall f \in F: f \in \Img G$
Thus by definition:
:$G$ is a surjection.
=== Order Embedding ===
Let $\RR, \QQ \in \map {\operatorname{Aux} } R$.
We will prove that:
:$\RR \precsim' \QQ \implies \map G \RR \preccurlyeq \map G \QQ$
Let:
:$\RR \precsim' \QQ$
By definition of $\precsim'$:
:$\RR \subseteq \QQ$
Let $x \in S$.
By Relation Segment is Increasing:
:$x^\RR \subseteq x^\QQ$
By Relation Segment of Auxiliary Relation is Ideal:
:$x^\RR \in \map {\operatorname{Ids} } R$ and $x^\QQ \in \map {\operatorname{Ids} } R$
By definition of $\precsim$:
:$x^\RR \precsim x^\QQ$
By definition of ordering on mappings:
:$\paren {S \ni x \mapsto x^\RR} \precsim \paren {S \ni x \mapsto x^\QQ}$
Thus by definitions of $G$ and $\preccurlyeq$:
:$\map G \RR \preccurlyeq \map G \QQ$
We will prove that:
:$\map G \RR \preccurlyeq \map G \QQ \implies \RR \precsim' \QQ$
Let:
:$\map G \RR \preccurlyeq \map G \QQ$
By definition of $G$ and $\preccurlyeq$:
:$\paren {S \ni x \mapsto x^\RR} \precsim \paren {S \ni x \mapsto x^\QQ}$
Let $x, y \in S$ such that:
:$\tuple {x, y} \in \RR$
By definition of $\RR$-segment:
:$x \in y^\RR$
By definition of ordering on mappings:
:$y^\RR \precsim y^\QQ$
By definition of $\precsim$:
:$y^\RR \subseteq y^\QQ$
By definition of subset:
:$x \in y^\QQ$
Thus by definition of $\QQ$-segment:
:$\tuple {x, y} \in \QQ$
By definition of subset:
:$\RR \subseteq \QQ$
Thus by definition of $\precsim'$:
:$\RR \precsim' \QQ$
== Sources ==
* 
* 
Category:Auxiliary Relations