nyuuzyou/wikis huggingface dataset:
Subset of Open Reciprocal-N Balls forms Neighborhood Basis in Real Number Line

== Theorem ==
Let $\R$ denote the real number line with the usual (Euclidean) metric.
Let $a \in \R$ be a point in $\R$.
Let $k \in \Z$ be some fixed integer.
Let $\BB_a$ be defined as:
:$\BB_a := \set {\map {B_\epsilon} a: \epsilon \in \set {\dfrac 1 n: n \in \N, n > k} }$
that is, the set of all open $\epsilon$-balls of $a$ for $\epsilon$ which are reciprocals of integers greater than $k$.
Then the $\BB_a$ is a basis for the neighborhood system of $a$.
== Proof ==
Let $N$ be a neighborhood of $a$ in $M$.
Then by definition:
:$\exists \epsilon' \in \R_{>0}: \map {B_{\epsilon'} } a \subseteq N$
where $\map {B_{\epsilon'} } a$ is the open $\epsilon'$-ball at $a$.
From Open Ball in Real Number Line is Open Interval:
:$\map {B_{\epsilon'} } a = \openint {a - \epsilon'} {a + \epsilon'}$
From Between two Real Numbers exists Rational Number:
:$\exists \epsilon \in \Q: 0 < \epsilon < \epsilon'$
Let $\epsilon$ be expressed in canonical form:
:$\epsilon = \dfrac p q$
Let $\epsilon = \dfrac 1 q$
Then $\epsilon' \le \epsilon < \epsilon'$
If $q \le k$, let $\epsilon = \dfrac 1 {k + 1}$
Otherwise, let $\epsilon = \epsilon$.
Then:
:$\openint {a - \epsilon} {a + \epsilon} \subseteq \openint {a - \epsilon'} {a + \epsilon'}$
From Open Real Interval is Open Ball
:$\map {B_\epsilon} a = \openint {a - \epsilon} {a + \epsilon}$
is the open $\epsilon$-ball at $a$.
By its method of construction:
:$\map {B_\epsilon} a \in \set {\map {B_\epsilon} a: \epsilon \in \set {\dfrac 1 n: n \in \N, n > k} }$
From Subset Relation is Transitive:
:$\openint {a - \epsilon} {a + \epsilon} \subseteq N$
From Open Ball is Neighborhood of all Points Inside, $\openint {a - \epsilon} {a + \epsilon}$ is a neighborhood of $a$ in $M$.
Hence the result by definition of basis for the neighborhood system of $a$.
== Sources ==
* : Chapter $2$: Metric Spaces: $\S 4$: Open Balls and Neighborhoods: Exercise $4 \ \text{iv)}$
Category:Real Intervals
Category:Real Number Line with Euclidean Metric
Subset of Ordinal implies Cardinal Inequality

== Theorem ==
Let $S$ be a set.
Let $x$ be an ordinal such that $S \subseteq x$.
Then:
:$\card S \le \card x$
where $\card S$ denotes the cardinality of $S$.
== Proof ==
Since $x$ is an ordinal, it follows that $x \sim \card x$ by Ordinal Number Equivalent to Cardinal Number.
This satisfies the hypothesis for Subset implies Cardinal Inequality.
Therefore:
:$\card S \le \card x$
== Sources ==
* : $\S 10.23$
Category:Cardinals
Subset of Ordinals has Minimal Element

== Theorem ==
Let $A$ be an ordinal (we shall allow $A$ to be a proper class).
Let $B$ be a nonempty subset of $A$.
Then $B$ has an $\Epsilon$-minimal element.
That is:
:$\exists x \in B: B \cap x = \O$
== Proof ==
We have that $\Epsilon$ creates a well-ordering on any ordinal.
Also, the initial segments of $x$ are sets.
Therefore from Proper Well-Ordering Determines Smallest Elements:
:$B$ has an $\Epsilon$-minimal element.
== Sources ==
* : $\S 7.5$
Category:Class Theory
Category:Ordinals
Subset of Particular Point Space is either Open or Closed

== Theorem ==
Let $T = \struct {S, \tau_p}$ be a particular point space.
Let $H \subseteq S$ be any subset of $T$.
Then $H$ is either open or closed in $T$.
The only sets which are both closed and open in $T$ are $S$ and $\O$.
== Proof ==
Let $H \subseteq S$.
There are two cases to consider:
:$p \in H$
:$p \notin H$
If $p \in H$ then by definition of a particular point topology, $H$ is open.
If $p \notin H$, then $p \in \relcomp S H$, where $\relcomp S H$ is the relative complement of $H$ in $S$.
So $\relcomp S H$ is open by definition of a particular point topology.
From the definition of a closed set, $\relcomp S {\relcomp S H}$ is closed in $T$.
From Relative Complement of Relative Complement we have that $\relcomp S {\relcomp S H} = H$ and so $H$ is closed in $T$.
Now suppose $H \subseteq T$ is both closed and open in $T$.
From Open and Closed Sets in Topological Space, if $H = \O$ or $H = S$ then H is both closed and open in $T$.
So, suppose $H \ne \O$ or $H \ne S$.
As $H \subseteq T$ is both closed and open in $T$, $\relcomp S H$ is also both closed and open in $T$.
From Boundary is Intersection of Closure with Closure of Complement we have:
:$\partial H = H^- \cap \paren {\relcomp S H}^-$
where $H^-$ is the closure of $H$.
By Closure of Open Set of Particular Point Space we have that $H^- = S$, and of course $\paren {\relcomp S H}^- = S$.
So:
:$\partial H = H^- \cap \paren {\relcomp S H}^- = S$
However, from Set Clopen iff Boundary is Empty we have that $\partial H = \O$.
Hence if $H$ is both closed and open in $T$, then $H = \O$ or $H = S$.
Category:Open Sets
Category:Closed Sets
Category:Clopen Sets
Category:Particular Point Topology
Subset of Preimage under Relation is Preimage of Subset

== Theorem ==
Let $\RR \subseteq S \times T$ be a relation.
Let $X \subseteq S, Y \subseteq T$.
Then:
:$X \subseteq \RR^{-1} \sqbrk Y \iff \RR \sqbrk X \subseteq Y$
In the language of direct image mappings, this can be written:
:$X \subseteq \map {\RR^\gets} Y \iff \map {\RR^\to} X \subseteq Y$
=== Corollary ===
If $f: S \to T$ is a mapping, the same result holds:
== Proof ==
As $\RR$ is a relation, then so is its inverse $\RR^{-1}$.
Let $\RR \sqbrk X \subseteq Y$.
Thus:
So:
:$\RR \sqbrk X \subseteq Y \implies X \subseteq \RR^{-1} \sqbrk Y$
Now let $X \subseteq \RR^{-1} \sqbrk Y$.
The same argument applies:
So:
:$X \subseteq \RR^{-1} \sqbrk Y \implies \RR \sqbrk X \subseteq Y$
Thus we have:
:$X \subseteq \RR^{-1} \sqbrk Y \implies \RR \sqbrk X \subseteq Y$
:$\RR \sqbrk X \subseteq Y \implies X \subseteq \RR^{-1} \sqbrk Y$
Hence the result.
Category:Subsets
Category:Preimages under Relations
Subset of Preimage under Relation is Preimage of Subset/Corollary

== Corollary to Subset of Preimage under Relation is Preimage of Subset ==
Let $f: S \to T$ be a mapping.
Let $X \subseteq S, Y \subseteq T$.
Then:
:$X \subseteq f^{-1} \sqbrk Y \iff f \sqbrk X \subseteq Y$
This can be expressed in the language and notation of direct image mappings and inverse image mappings as:
:$\forall X \in \powerset S, Y \in \powerset T: X \subseteq \map {f^\gets} Y \iff \map {f^\to} X \subseteq Y$
== Proof ==
Let $f: S \to T$ be a mapping.
As a mapping is also a relation, it follows that $f$ is a relation and so:
:$X \subseteq f^{-1} \sqbrk Y \iff f \sqbrk X \subseteq Y$
holds on the strength of Subset of Preimage under Relation is Preimage of Subset.
== Sources ==
* : $\S 5$. Induced mappings; composition; injections; surjections; bijections: Theorem $5.1 \ \text{(v)}$
Category:Subsets
Category:Preimages under Mappings
Subset of Real Numbers is Interval iff Connected

== Theorem ==
Let the real number line $\R$ be considered as a topological space.
Let $S$ be a subspace of $\R$.
Then $S$ is connected $S$ is an interval of $\R$.
That is, the only subspaces of $\R$ that are connected are intervals.
== Proof ==
From Rule of Transposition, we may replace the only if statement by its contrapositive.
Therefore, the following suffices:
=== Sufficient Condition ===
Suppose $S$ is an interval of $\R$.
Suppose further that $A \mid B$ is a separation of $S$.
Let $a \in A, b \in B$.
, suppose that $a < b$.
Since $a, b \in S$, and $S$ is an interval, $\closedint a b \subseteq S$.
Let $A' = A \cap \closedint a b$ and $B' = B \cap \closedint a b$.
Then:
By the definition of a separation, both $A$ and $B$ are closed in $S$.
Hence by Closed Set in Topological Subspace, $A'$ and $B'$ are also closed in $\closedint a b$.
From Closed Set in Topological Subspace: Corollary, $A'$ and $B'$ are closed in $\R$.
Now, since $B' \ne \O$, and $B$ is bounded below (by, for example, $a$), by the Continuum Property $b' := \map \inf {B'}$ exists, and $b' \ge a$.
We have that $B'$ is closed in $\R$
Hence from Closure of Real Interval is Closed Real Interval:
:$b' \in B'$
Since $a \in A'$ and $A \cap B = \O$, it follows that $b' > a$.
Now let $A = A' \cap \closedint a {b'}$.
Using the same argument as for $B'$, we have that $a = \map \sup {A}$ exists, that $a \in A$ and also $a < b'$.
Now $\openint {a} {b'} \cap A' = \O$ or $a$ would not be an upper bound for $A$.
Similarly, $\openint {a} {b'} \cap B' = \O$ or $b'$ would not be a lower bound for $B$.
Thus:
:$\openint {a} {b'} \cap \paren {A' \cup B'} = \O$
But since $a < a < b' < b$, we also have:
:$\openint {a} {b'} \subseteq \closedint a b$, and
:$\openint {a} {b'}$ is non-empty.
So, there is an element $z \in \openint {a} {b'}$, and hence in $\closedint a b$, which is not in $A' \cup B'$.
This contradicts $(1)$ above, which says that we have $A' \cup B' = \closedint a b$.
From this contradiction it follows that there can be no such separation $A \mid B$ on the interval $S$.
Therefore, by definition, $S$ is connected.
=== Necessary Condition ===
Suppose $S$ is not an interval of $\R$.
Then $\exists x, y \in S$ and $z \in \R \setminus S$ such that $x < z < y$.
Consider the sets $S \cap \openint \gets z$ and $S \cap \openint z \to$.
Then $S \cap \openint \gets z$ and $S \cap \openint z \to$ are open by definition of the subspace topology on $S$.
Neither is empty because they contain $x$ and $y$ respectively.
They are disjoint, and their union is $S$, since $z \notin S$.
Therefore $S \cap \openint \gets z \mid S \cap \openint z \to$ is a separation of $S$.
It follows by definition that $S$ is disconnected.
== Sources ==
* : $6.2$: Connectedness: Theorem $6.2.7$, $6.2.8$
Category:Real Intervals
Category:Connected Spaces
Subset of Real Numbers is Path-Connected iff Interval

== Theorem ==
Let $\R$ be the real number line considered as an Euclidean space.
Let $S \subseteq \R$ be a subset of $\R$.
Then $S$ is a path-connected metric subspace of $\R$ $S$ is a real interval.
== Proof ==
=== Necessary Condition ===
Let $S$ be a path-connected metric subspace of $\R$.
From Path-Connected Space is Connected, it follows that $S$ is connected.
From Subset of Real Numbers is Interval iff Connected, it follows that $S$ is a real interval.
=== Sufficient Condition ===
Let $S$ be a real interval.
== Sources ==
* : Chapter $\text{III}$: Metric Spaces: Path-Connectedness
Category:Path-Connected Spaces
Subset of Satisfiable Set is Satisfiable

== Theorem ==
Let $\LL$ be a logical language.
Let $\mathscr M$ be a formal semantics for $\LL$.
Let $\FF$ be an $\mathscr M$-satisfiable set of formulas from $\LL$.
Let $\FF'$ be a subset of $\FF$.
Then $\FF'$ is also $\mathscr M$-satisfiable.
== Proof ==
Since $\FF$ is $\mathscr M$-satisfiable, there exists some model $\MM$ of $\FF$:
:$\MM \models_{\mathscr M} \FF$
Thus for every $\psi \in \FF$:
:$\MM \models_{\mathscr M} \psi$
Now, for every $\psi$ in $\FF'$:
:$\psi \in \FF$
by definition of subset.
Hence:
:$\forall \psi \in \FF': \MM \models_{\mathscr M} \psi$
that is, $\MM$ is a model of $\FF'$.
Hence $\FF'$ is $\mathscr M$-satisfiable.
Category:Formal Semantics
Subset of Set Difference iff Disjoint Set

== Theorem ==
Let $S, T$ be sets.
Let $A \subseteq S$
Then:
:$A \cap T = \O \iff A \subseteq S \setminus T$
where:
:$A \cap T$ denotes set intersection
:$\O$ denotes the empty set
:$S \setminus T$ denotes set difference.
== Proof ==
We have:
Then:
Category:Set Difference
Category:Disjoint Sets
Subset of Set is Coarser than Set

== Theorem ==
Let $\left({S, \preceq}\right)$ be a preordered set.
Let $A, B$ be subset of $S$ such that
:$A \subseteq B$
Then $A$ is coarser than $B$.
== Proof ==
Let $x \in A$.
By definition of subset:
:$x \in B$
By definition of reflexivity:
:$x \preceq x$
Thus
:$\exists y \in B: y \preceq x$
== Sources ==
* 
Category:Preorder Theory
Subset of Set with Propositional Function

== Theorem ==
Let $S$ be a set.
Let $P: S \to \set {\T, \F}$ be a propositional function on $S$.
Then:
:$\set {x \in S: \map P x} \subseteq S$
== Proof ==
== Sources ==
* : Chapter $1$: The Notation and Terminology of Set Theory: $\S 4$
* : Notation and Terminology
Category:Subsets
Category:Mapping Theory
Subset of Sigma-Locally Finite Set of Subsets is Sigma-Locally Finite

== Theorem ==
Let $T = \struct{S, \tau}$ be a topological space.
Let $\FF \subseteq \powerset S$ be a set of subsets of $S$.
Let $\GG \subseteq \FF$.
If $\FF$ is $\sigma$-locally finite then $\GG$ is $\sigma$-locally finite.
== Proof ==
By definition of $\sigma$-locally finite:
:$\FF = \ds \bigcup_{n \in \N} \FF_n$
where $\FF_n$ is locally finite for each $n \in \N$.
For each $n \in \N$, let:
:$\GG_n = \GG \cap \FF_n$
We have:
From Intersection is Subset:
:$\GG_n \subseteq \FF_n$
From Subset of Locally Finite Set of Subsets is Locally Finite:
:$\GG_n$ is locally finite for each $n \in \N$
By definition, $\GG$ is $\sigma$-locally finite.
Category:Sigma-Locally Finite Sets of Subsets
Subset of Standard Discrete Metric Space is Neighborhood of Each Point

== Theorem ==
Let $M = \struct {A, d}$ be a metric space where $d$ is the standard discrete metric.
Let $S \subseteq A$.
Let $a \in S$.
Then $S$ is a neighborhood of $a$.
That is, every subset of $A$ is a neighborhood of each of its points. 
== Proof ==
Let $S \subseteq A$.
Let $a \in S$.
From Neighborhoods in Standard Discrete Metric Space, $\set a$ is a neighborhood of $a$.
As $a \in S$ it follows from Singleton of Element is Subset that $\set a \subseteq S$.
The result follows from Superset of Neighborhood in Metric Space is Neighborhood.
== Sources ==
* : Chapter $2$: Metric Spaces: $\S 4$: Open Balls and Neighborhoods: Exercise $1$
Category:Standard Discrete Metric
Category:Neighborhoods
Subset of Standard Discrete Metric Space is Open

== Theorem ==
Let $M = \struct {A, d}$ be a standard discrete metric space.
Let $S \subseteq A$ be a subset of $A$.
Then $S$ is an open set of $M$.
== Proof ==
From the definition of standard discrete metric:
:$\forall x, y \in A: \map d {x, y} = \begin {cases} 0 & : x = y \\ 1 & : x \ne y \end {cases}$
Let $\epsilon \in \R_{>0}$ be such that $0 < \epsilon \le 1$.
Let $x \in S$.
Let $\map {B_\epsilon} x$ be the open $\epsilon$-ball of $x$.
Then by definition of $\epsilon$ and $d$:
:$\map {B_\epsilon} x = \set x$
Thus:
:$\forall x \in S: \map {B_\epsilon} x \subseteq S$
Hence the result by definition of open set.
== Sources ==
* : Chapter $2$: Metric Spaces: $\S 6$: Open Sets and Closed Sets: Exercise $2$
* : $2$: Continuity generalized: metric spaces: $2.3$: Open sets in metric spaces: Example $2.3.11$
Category:Standard Discrete Metric
Subset of Toset is Toset

== Theorem ==
Let $\left({S, \preceq}\right)$ be a totally ordered set.
Let $T \subseteq S$.
Then $\left({T, \preceq \restriction_T}\right)$ is also a totally ordered set.
In the above, $\preceq \restriction_T$ denotes the restriction of $\preceq$ to $T$.
== Proof ==
As $\left({S, \preceq}\right)$ is a totally ordered set, the relation $\preceq$ is a total ordering, and is by definition:
* reflexive
* antisymmetric
* transitive
* connected
From Properties of Restriction of Relation, a restriction of a relation which has all those properties inherits them all.
Thus $\preceq \restriction_T$ is also:
* reflexive
* antisymmetric
* transitive
* connected
and so is also a total ordering.
Hence the result, by definition of totally ordered set.
== Sources ==
* : $\S 3.3$: Ordered sets. Order types
Category:Total Orderings
Subset of Well-Founded Relation is Well-Founded

== Theorem ==
Let $\struct {S, \RR}$ be a relational structure.
Let $\RR$ be a well-founded relation on $S$.
Let $\QQ$ be a subset of $\RR$.
Then $\QQ$ is also a well-founded relation on $S$.
== Proof ==
 $\struct {S, \QQ}$ is not a well-founded set.
By Infinite Sequence Property of Well-Founded Relation there exists an infinite sequence $\sequence {x_n}$ in $S$ such that:
:$\forall n \in \N: \tuple {x_{n + 1}, x_n} \in \QQ \text { and } x_{n + 1} \ne x_n$
But then because $\QQ \subseteq \RR$, it follows that:
:$\forall n \in \N: \tuple {x_{n + 1}, x_n} \in \QQ \implies \tuple {x_{n + 1}, x_n} \in \RR$
and it follows that:
:$\forall n \in \N: \tuple {x_{n + 1}, x_n} \in \RR \text { and } x_{n + 1} \ne x_n$
Hence by Infinite Sequence Property of Well-Founded Relation it follows that $\RR$ is not a well-founded relation on $S$.
The result follows by Proof by Contradiction.
== Sources ==
* : Part $1$: Not Entirely Naive Set Theory: Chapter $2$: Partial Order Relations: Exercise $15 \ \text {(a)}$
Category:Well-Founded Relations
Subset of Well-Ordered Set is Well-Ordered

== Theorem ==
Let $\struct {S, \preceq}$ be a well-ordered set.
Let $T \subseteq S$ be a subset of $S$.
Let $\preceq'$ be the restriction of $\preceq$ to $T$.
Then the relational structure $\struct {T, \preceq'}$ is a well-ordered set.
== Proof 1 ==
== Proof 2 ==
== Proof 3 ==
== Sources ==
* : Chapter $\text {III}$: The Natural Numbers: $\S 14$: Orderings
* : $\S 3.5$: Well-ordered sets. Ordinal Numbers: Example $2$
* : Appendix $\text{A}.6$: Mathematical Induction: Problem Set $\text{A}.6$: $34$
Category:Well-Orderings
Category:Subset of Well-Ordered Set is Well-Ordered
Subset of Well-Ordered Set is Well-Ordered/Proof 1

== Theorem ==
== Proof ==
First suppose that $T = \O$.
From Empty Set is Subset of All Sets, $T$ is a subset of $S$.
By Empty Set is Well-Ordered, $\struct {\O, \preceq'}$ is a well-ordered set. 
Otherwise, let $T$ be non-empty.
Let $X \subseteq T$ such that $X \ne \O$ be arbitrary.
Such a subset exists, as from Set is Subset of Itself, $T$ itself is a subset of $T$.
By Subset Relation is Transitive, $X \subseteq S$.
By the definition of a well-ordered set, $X$ has a smallest element under $\preceq$.
That is:
:$\forall y \in S: x \preceq y$
Hence as $T \subseteq S$:
:$\forall y \in T: x \preceq y$
Because $\preceq'$ is the restriction of $\preceq$ to $T$:
:$\forall y \in T: x \preceq' y$
and so $x$ is the smallest element of $X$ under $\preceq'$.
It follows by definition that $\struct {T, \preceq'}$ is a well-ordered set.
Category:Subset of Well-Ordered Set is Well-Ordered
Subset of Well-Ordered Set is Well-Ordered/Proof 2

== Theorem ==
== Proof ==
By definition of well-ordered set, $\struct {S, \preceq}$ is:
:a totally ordered set
and:
:a well-founded set.
By Subset of Toset is Toset, $\struct {T, \preceq'}$ is a totally ordered set.
By Subset of Well-Founded Relation is Well-Founded, $\preceq'$ is a well-founded relation.
Hence the result.
== Sources ==
* : Part $1$: Not Entirely Naive Set Theory: Chapter $2$: Partial Order Relations: Exercise $15 \ \text {(b)}$
Category:Subset of Well-Ordered Set is Well-Ordered
Subset of Well-Ordered Set is Well-Ordered/Proof 3

== Theorem ==
== Proof ==
Let $V$ be a basic universe.
By definition of basic universe, $S$ and $T$ are all elements of $V$.
By the , $S$ and $T$ are both classes.
Thus $T$ is a subclass of $S$.
We have that $\preceq$ is a well-ordering on $S$.
So from Subclass of Well-Ordered Class is Well-Ordered, $\preceq'$ is a well-ordering on $T$.
Hence the result.
Category:Subset of Well-Ordered Set is Well-Ordered
Subset of von Neumann-Bounded Set is von Neumann-Bounded

== Definition ==
Let $\Bbb F \in \set {\R, \C}$.
Let $\struct {X, \tau}$ be a topological vector space over $\Bbb F$.
Let $E \subseteq X$ be von Neumann-bounded.
Let $F \subseteq X$.
Then $F$ is von Neumann-bounded.
== Proof ==
Let $V$ be an open neighborhood of ${\mathbf 0}_X$.
Then there exists $s > 0$ such that: 
:$E \subseteq t V$ for each $t > s$. 
Then: 
:$F \subseteq t V$ for each $t > s$. 
Category:Von Neumann-Bounded Subsets of Topological Vector Spaces
Subsets Greater Than and Less Than Identity of Ordered Abelian Group are Isomorphic Ordered Semigroups

== Theorem ==
Let $\struct {G, \circ, \preccurlyeq}$ be an ordered abelian group whose identity element is $e$.
Let $G^+$ and $G^-$ denote the subsets of $G$ defined as:
:$G^+ = \set {x \in G: e \preccurlyeq x}$
:$G^- = \set {x \in G: x \preccurlyeq e}$
Then $\struct {G^+, \circ, \preccurlyeq}$ and $\struct {G^-, \circ, \succcurlyeq}$ are subsemigroups of $G$ such that the inversion mapping $\iota: G \to G$ defined as:
:$\forall g \in G: \map \iota g = g^{-1}$
is:
:an isomorphism from $\struct {G^+, \circ, \preccurlyeq}$ to $\struct {G^-, \circ, \succcurlyeq}$
and:
:an isomorphism from $\struct {G^-, \circ, \preccurlyeq}$ to $\struct {G^+, \circ, \succcurlyeq}$
== Proof ==
Let $x, y \in G^+$ be arbitrary.
Then:
So by the Subsemigroup Closure Test $\struct {G^+, \circ}$ is a subsemigroup of $\struct {G, \circ}$.
Let $x, y \in G^-$ be arbitrary.
Then:
So by the Subsemigroup Closure Test $\struct {G^-, \circ}$ is a subsemigroup of $\struct {G, \circ}$.
Then we establish that:
demonstrating that for all $\iota$ has the morphism property over the whole of $G$.
Then we note that:
Similarly:
Then we note that:
demonstrating that $\iota$ is an injection.
Let $x \in G^+$.
Then :
:$\exists x^{-1} \in G^-: \map \iota {x^{-1} } = x$
Similarly, let $x \in G^-$.
Then :
:$\exists x^{-1} \in G^+: \map \iota {x^{-1} } = x$
So $\iota: G^+ \to G^-$ and $\iota: G^- \to G^+$ are both surjections.
Hence $\iota: G^+ \to G^-$ and $\iota: G^- \to G^+$ are both bijections by definition.
Thus we have that:
:$\iota: \struct {G^+, \circ} \to \struct {G^-, \circ}$ is a semigroup isomorphism
and
:$\iota: \struct {G^-, \circ} \to \struct {G^+, \circ}$ is a semigroup isomorphism.
Let $x, y \in G^+$ be arbitrary, such that $x \preccurlyeq y$.
We have:
Let $x, y \in G^-$ be arbitrary, such that $x \succcurlyeq y$.
We have:
Thus we have demonstrated that $\iota: \struct {G^+, \preccurlyeq} \to \struct {G^-, \succcurlyeq}$ and $\iota: \struct {G^-, \succcurlyeq} \to \struct {G^+, \preccurlyeq}$ are order isomorphisms.
So we have that:
Thus we have that:
:$\iota: \struct {G^+, \circ} \to \struct {G^-, \circ}$ is a semigroup isomorphism
:$\iota: \struct {G^+, \preccurlyeq} \to \struct {G^-, \succcurlyeq}$ is an order isomorphism
and so:
:$\iota: \struct {G^+, \circ, \preccurlyeq} \to \struct {G^-, \circ, \succcurlyeq}$ is an ordered semigroup isomorphism
and
:$\iota: \struct {G^-, \circ} \to \struct {G^+, \circ}$ is a semigroup isomorphism
:$\iota: \struct {G^-, \succcurlyeq} \to \struct {G^+, \preccurlyeq}$ is an order isomorphism
and so:
:$\iota: \struct {G^-, \circ, \succcurlyeq} \to \struct {G^+, \circ, \preccurlyeq}$ is an ordered semigroup isomorphism
== Sources ==
* : Chapter $\text {III}$: The Natural Numbers: $\S 15$: Ordered Semigroups: Exercise $15.4$
Category:Ordered Groups
Category:Abelian Groups
Category:Inversion Mappings
Category:Ordered Semigroup Isomorphisms
Subsets Satisfy Formulation 1 Matroid Base Axiom Iff Complements Satisfy Formulation 5

== Theorem ==
Let $S$ be a finite set.
Let $\mathscr B$ be a non-empty set of subsets of $S$.
Let $\mathscr B^* = \set{S \setminus B : B \in \mathscr B}$.
Then:
:$\mathscr B$ satisfies formulation $1$ base axiom:
:$\mathscr B^*$ satisfies formulation $5$ base axiom:
== Proof ==
=== Necessary Condition ===
Let $\mathscr B$ satisfies formulation $1$ base axiom:
Let $B^*_1, B^*_2 \in \mathscr B^*$.
By definition of $\mathscr B^*$:
:$\exists B_1, B_2 \in \mathscr B$: 
::$B^*_1 = S \setminus B_1$
::$B^*_2 = S \setminus B_2$
We have:
And similarly:
:$B^*_2 \setminus B^*_1 = B_1 \setminus B_2$
Let $x \in B^*_1 \setminus B^*_2$.
Hence:
:$x \in B_2 \setminus B_1$
From formulation $1$ base axiom:
:$\exists y \in B_1 \setminus B_2 : \paren{B_2 \setminus \set x} \cup \set y \in \mathscr B$
Hence:
:$y \in B^*_2 \setminus B^*_1$
We have:
Hence:
:$\paren{B^*_2 \setminus \set y} \cup \set x \in \mathscr B^*$
It follows that $\mathscr B^*$ satisfies formulation 5 base axiom:
=== Sufficient Condition ===
Let $\mathscr B^*$ satisfies formulation $5$ base axiom:
Let $B_1, B_2 \in \mathscr B$.
By definition of $\mathscr B^*$:
:$\exists B^*_1, B^*_2 \in \mathscr B^*$: 
::$B^*_1 = S \setminus B_1$
::$B^*_2 = S \setminus B_2$
We have:
And similarly:
:$B^*_2 \setminus B^*_1 = B_1 \setminus B_2$
Let $x \in B_1 \setminus B_2$.
Hence:
:$x \in B^*_2 \setminus B^*_1$
From formulation $5$ base axiom:
:$\exists y \in B^*_1 \setminus B^*_2 : \paren{B^*_1 \setminus \set y} \cup \set x \in \mathscr B^*$
Hence:
:$y \in B_2 \setminus B_1$
By definition of $\mathscr B^*$:
:$\exists B_3 \in \mathscr B : S \setminus B_3 = \paren{B^*_1 \setminus \set y} \cup \set x$
We have:
Hence:
:$\paren{B_1 \setminus \set y} \cup \set x \in \mathscr B$
It follows that $\mathscr B$ satisfies formulation 1 base axiom:
== Also see ==
* Subsets Satisfy Formulation 5 Matroid Base Axiom Iff Complements Satisfy Formulation 1
Category:Matroid Bases