avewright/proofwiki-math huggingface dataset:
Theorem: Jordan Polygon Theorem

Let $P$ be a polygon embedded in $\R^2$.
Denote the boundary of $P$ as $\partial P$.
Then, $\R^2 \setminus \partial P$ is a union of two connected components.
Both components are open in $\R^2$.
One component is bounded, and is called the interior of $P$.
The other component is unbounded, and is called the exterior of $P$.

Proof:
=== Lemma ===
{{:Jordan Polygon Theorem/Lemma 1}}{{qed|lemma}}
We show that $\R^2 \setminus \partial P$ is not path-connected.
Find any $q_1 \in R^2 \setminus \partial P$ and $\theta \in \R$ such that the ray $\LL_\theta = \set {q_1 + s \map g \theta: s \in \R_{\ge 0} }$ has exactly one crossing of $\partial P$.
Find any $q_2 \in \LL_\theta$ that lies on the ray after the crossing, so the ray $\set {q_2 + s \map g \theta: s \in \R_{\ge 0} }$ does not intersect $\partial P$.
Then $\map {\mathrm {par} } {q_1} = 1 \ne 0 = \map {\mathrm {par} } {q_2}$.
From Jordan Polygon Parity Lemma, it follows that $q_1$ and $q_2$ cannot be connected by a path.
{{qed|lemma}}
As $R^2 \setminus \partial P$ is not path-connected, it follows from {{Lemma|Jordan Polygon Theorem|1}} that $R^2 \setminus \partial P$ is a union of exactly two disjoint path-connected sets, which we denote as $U_1$ and $U_2$.
Let $q \in \R^2 \setminus \partial P$, and let $\map d {q, \partial P}$ be the Euclidean distance between $q$ and $\partial P$.
From Distance between Closed Sets in Euclidean Space, it follows that $\map d {q, \partial P} > 0$.
When we put $\epsilon = \map d {q, \partial P} / 2$, we have $\map {B_\epsilon} q \subseteq \R^2 \setminus \partial P$.
As Open Ball is Convex Set, it follows that $\map {B_\epsilon} q$ is path-connected, so $\map {B_\epsilon} q$ is a subset of either $U_1$ or $U_2$.
Then, both $U_1$ and $U_2$ are open.
From Path-Connected Space is Connected, it follows that $U_1$ and $U_2$ are connected.
Then, $\R^2 \setminus \partial P$ is a union of two components.
{{qed|lemma}}
From Boundary of Polygon is Jordan Curve, it follows that $\partial P$ is equal to the image of a Jordan curve $\gamma: \closedint 0 1 \to \R^2$.
From {{Corollary|Continuous Image of Compact Space is Compact|2}}, it follows that $\partial P$ is bounded.
That is, there exist $a \in \R^2$ and $R \in \R_{>0}$ such that $\partial P \subseteq \map {B_R} a$.
If $x_1, x_2 \in \R^2 \setminus \map {B_R} a$, $x_1$ to $x_2$ can be joined by a path in $\R^2 \setminus \map {B_R} a$ following:
:the circumference of the two circles with center $a$ and radii $\map d {a, x_1}$ and $\map d {a, x_2}$
:a line segment joining the two circumferences.
Then $\R^2 \setminus \map {B_R} a$ is path-connected, so $\R^2 \setminus \map {B_R} a$ is a subset of one of the components of $\R^2 \setminus \partial P$, say $U_1$.
As $\R^2 \setminus \map {B_R} a \subseteq U_1$, it follows that $U_1$ is unbounded, so $U_1$ is the exterior of $\gamma$.
Then $U_2 \subseteq \map {B_R} a$, so $U_2$ is bounded, which implies that $U_2$ is the interior of $\gamma$.
{{qed}}
{{Namedfor|Marie Ennemond Camille Jordan|cat = Jordan, C}}
Theorem: Jordan Polygon Interior and Exterior Criterion

Let $P$ be a polygon embedded in $\R^2$.
Let $q \in \R^2 \setminus \partial P$, where $\partial P$ denotes the boundary of $P$.
Let $\mathbf v \in \R^2 \setminus \set \bszero$ be a non-zero vector.
Let $\LL = \set {q + s \mathbf v: s \in \R_{\ge 0} }$ be a ray with start point $q$.
Let $\map N q \in \N$ be the number of crossings between $\LL$ and $\partial P$.
Then:
:$(1): \quad$ $q \in \Int P$, {{iff}} $\map N q \equiv 1 \pmod 2$
:$(2): \quad$ $q \in \Ext P$, {{iff}} $\map N q \equiv 0 \pmod 2$
Here, $\Int P$ and $\Ext P$ denote the interior and exterior of $\partial P$, when $\partial P$ is considered as a Jordan curve.

Proof:
From Boundary of Polygon is Jordan Curve, it follows that $\partial P$ is equal to the image of a Jordan curve.
From the Jordan Polygon Theorem, it follows that $\Int P$ and $\Ext P$ are path-connected.
Then, Jordan Polygon Parity Lemma shows that $\map N q = \map {\operatorname{par} } q$, where $\map {\operatorname{par} } q$ denotes the parity of $q$.
From Jordan Polygon Theorem, it follows that $\Ext P$ is unbounded, while $\Int P$ is bounded.
As $\partial P$ is the image of a Jordan curve, it follows from {{Corollary|Continuous Image of Compact Space is Compact|2}} that $\partial P$ is also bounded.
Let $\map {B_R} \bszero$ be the open ball with radius $R$ and center $\bszero$.
Then, there exists $R \in \R_{>0}$ such that $\Int P \cup \partial P \subseteq \map {B_R} \bszero$.
If $q_0 \in \R^2 \setminus \map {B_R} \bszero$, then $q_0 \in \Ext P$.
Then, the ray $\set {q_0 + s q_0: s \in \R_{\ge 0} } \subseteq \R^2 \setminus \map {B_R} \bszero$, so there are zero crossings between the ray and $\partial P$.
From Jordan Polygon Parity Lemma, it follows that $\map {\operatorname{par} } {q_0} = 0$.
As $\Ext P$ is path-connected, it follows from the lemma that for all $q \in \Ext P$, we have $\map {\operatorname{par} } q = 0$.
If $q_1 \in \R^2 \setminus \partial P$ with $\map {\operatorname{par} } q = 1$, it follows that $q_1 \notin \Ext P$.
As $\R^2 \setminus \partial P = \Int P \cup \Ext P$, it follows that $q_1 \in \Int P$.
From Jordan Polygon Parity Lemma:
:$\forall q \in \Int P: \map {\operatorname{par} } q = 1$
So if instead $q_0 \in \R^2 \setminus \partial P$ with $\map {\operatorname{par} } q = 0$, the only possibility is that $q_0 \in \Ext P$.
{{qed}}
Theorem: Closed Set in Linearly Ordered Space

Let $\struct {X, \preceq, \tau}$ be a linearly ordered space.
Let $C$ be a subset of $X$.
Then $C$ is closed in $X$ {{iff}} for all non-empty subsets $S$ of $C$:
:If $s \in X$ is a supremum or infimum of $S$ in $X$, then $s \in C$.

Proof:
=== Necessary Condition ===
Suppose that $C$ be closed.
Let $S$ be a non-empty subset of $C$.
Let $b \in X \setminus C$.
We will show that $b$ is not a supremum of $S$.
If $b$ is not an upper bound of $S$, then by definition $b$ cannot be a supremum of $S$.
Suppose, then, that $b$ is an upper bound of $S$.
Since $C$ is closed and $b \notin C$, there must be an open interval or open ray $U$ containing $b$ that is disjoint from $Y$.
Since $b$ is an upper bound for $S$ and $S$ is non-empty, $U$ cannot be a downward-pointing ray.
Thus $U$ is either an open interval $\openint a q$ or an upward-pointing open ray ${\uparrow}a$.
Then:
:$a \prec b$
Since $b \in U$, and $b$ is an upper bound of $S$, no element strictly succeeding all elements of $U$ can be in $S$.
By the above and the fact that $S \subseteq C$, ${\uparrow}a \cap S = \O$, so $a$ is an upper bound of $S$.
Since $a \prec b$, $b$ is not a supremum of $S$.
A similar argument shows that $b$ is not an infimum.
{{qed|lemma}}
Theorem: Conditional is Left Distributive over Disjunction/Formulation 1/Forward Implication

:$p \implies \paren {q \lor r} \vdash \paren {p \implies q} \lor  \paren {p \implies r}$

Proof:
{{BeginTableau|p \implies \paren {q \lor r} \vdash \paren {p \implies q} \lor  \paren {p \implies r} }}
{{Assumption|1|p \implies \paren {q \lor r} }}
{{Assumption|2|p}}
{{ModusPonens|3|1, 2|q \lor r|1|2}}
{{IdentityLaw|4|2|p|2}}
{{Assumption|5|q}}
{{Implication|6|5|p \implies q|4|5}}
{{Addition|7|5|\paren {p \implies q} \lor \paren {p \implies r}|6|1}}
{{Assumption|8|r}}
{{SequentIntro|9|8|p \implies r|8|True Statement is implied by Every Statement}}
{{Addition|10|8|\paren {p \implies q} \lor \paren {p \implies r}|9|2}}
{{ProofByCases|11|1|\paren {p \implies q} \lor \paren {p \implies r}|3|2|7|8|10}}
{{EndTableau}}
{{qed}}
Category:Conditional is Left Distributive over Disjunction
cfe3ad6hi68e7fd8s3cx47b0ukww1j3
Theorem: Conditional is Left Distributive over Disjunction/Formulation 1/Reverse Implication

:$\paren {p \implies q} \lor \paren{p \implies r} \vdash p \implies \paren {q \lor r}$

Proof:
{{BeginTableau|\paren {p \implies q} \lor \paren {p \implies r} \vdash p \implies \paren {q \lor r} }}
{{Assumption|1|\paren {p \implies q} \lor \paren {p \implies r} }}
{{Assumption|2|p \implies q}}
{{Assumption|3|p}}
{{ModusPonens|4|2, 3|q|2|3}}
{{Addition|5|2, 3|q \lor r|4|1}}
{{Implication|6|2|p \implies \paren {q \lor r}|3|5}}
{{Assumption|7|p \implies r}}
{{Assumption|8|p}}
{{ModusPonens|9|7, 8|r|7|8}}
{{Addition|10|7, 8|q \lor r|9|2}}
{{Implication|11|7|p \implies \paren {q \lor r}|8|10}}
{{ProofByCases|12|1|p \implies \paren{q \lor r}|1|2|6|7|11}}
{{EndTableau}}
{{qed}}
Category:Conditional is Left Distributive over Disjunction
mymzyp8c8tm3rfwp2mf61e1ubabigk6
Theorem: Factor Principles/Disjunction on Left/Formulation 2

:$\vdash \paren {p \implies q} \implies \paren {\paren {r \lor p} \implies \paren {r \lor q} }$

Proof:
{{BeginTableau|\vdash \paren {p \implies q} \implies \paren {\paren {r \lor p} \implies \paren {r \lor q} } }}
{{Assumption|1|p \implies q}}
{{SequentIntro|2|1|\paren {\paren {r \lor p} \implies \paren {r \lor q} }|1|Factor Principles: Disjunction on Left: Formulation 1}}
{{Implication|3|1|\paren {p \implies q} \implies \paren {\paren {r \lor p} \implies \paren {r \lor q} }|1|2}}
{{EndTableau}}
{{qed}}
Theorem: Conditional is Left Distributive over Disjunction/Formulation 2

:$\vdash \paren {p \implies \paren {q \lor r} } \iff \paren {\paren {p \implies q} \lor \paren{p \implies r} }$

Proof:
{{BeginTableau|\vdash \paren {p \implies \paren {q \lor r} } \iff \paren {\paren {p \implies q} \lor \paren {p \implies r} } }}
{{Assumption|1|p \implies \paren {q \lor r} }}
{{SequentIntro|2|1|\paren {p \implies q} \lor \paren {p \implies r}|1|Conditional is Left Distributive over Disjunction: Formulation 1}}
{{Implication|3||\paren {p \implies \paren {q \lor r} } \implies \paren {\paren {p \implies q} \lor \paren {p \implies r} }|1|2}}
{{Assumption|4|\paren {p \implies q} \lor \paren {p \implies r} }}
{{SequentIntro|5|4|p \implies \paren {q \lor r}|4|Conditional is Left Distributive over Disjunction: Formulation 1}}
{{Implication|6||\paren {\paren {p \implies q} \lor \paren {p \implies r} } \implies \paren {p \implies \paren {q \lor r} }|4|5}}
{{BiconditionalIntro|7|3, 6|\paren {p \implies q} \lor \paren {p \implies r}|16|17|19|20|22}}
{{EndTableau}}
{{qed}}
Theorem: Factor Principles/Disjunction on Right/Formulation 2

:$\vdash \paren {p \implies q} \implies \paren {\paren {p \lor r} \implies \paren {q \lor r} }$

Proof:
{{BeginTableau|\vdash \paren {p \implies q} \implies \paren {\paren {p \lor r} \implies \paren {q \lor r} } }}
{{Assumption|1|p \implies q}}
{{SequentIntro|2|1|\paren {p \lor r} \implies \paren {q \lor r}|1
  |Factor Principles: Disjunction on Right: Formulation 1}}
{{Implication|3|1|\paren {p \implies q} \implies \paren {\paren {p \lor r} \implies \paren {q \lor r} }|1|2}}
{{EndTableau}}
{{qed}}
Theorem: Factor Principles/Disjunction on Right/Formulation 1

:$p \implies q \vdash \paren {p \lor r} \implies \paren {q \lor r}$

Proof:
{{BeginTableau|p \implies q \vdash \paren {p \lor r} \implies \paren {q \lor r} }}
{{Premise|1|p \implies q}}
{{TheoremIntro|2|r \implies r|Law of Identity: Formulation 2}}
{{SequentIntro|3|1|\paren {p \lor r} \implies \paren {q \lor r}|1, 2|Constructive Dilemma}}
{{EndTableau}}
{{qed}}
Theorem: Factor Principles/Disjunction on Right/Formulation 1

:$p \implies q \vdash \paren {p \lor r} \implies \paren {q \lor r}$

Proof:
{{BeginTableau|p \implies q \vdash \paren {p \lor r} \implies \paren {q \lor r} }}
{{Premise|1|p \implies q}}
{{Assumption|2|p \lor r}}
{{Assumption|3|r}}
{{Addition|4|3|q \lor r|3|2}}
{{Assumption|5|p}}
{{ModusPonens|6|1, 5|q|1|5}}
{{Addition|7|1, 5|q \lor r|6|1}}
{{ProofByCases|8|1, 2|q \lor r|2|5|7|3|4}}
{{Implication|9|1|\paren {p \lor r} \implies \paren {q \lor r}|2|8}}
{{EndTableau}}
{{qed}}
Theorem: Factor Principles/Disjunction on Right/Formulation 1

:$p \implies q \vdash \paren {p \lor r} \implies \paren {q \lor r}$

Proof:
{{BeginTableau|p \implies q \vdash \paren {p \lor r} \implies \paren {q \lor r} }}
{{Premise|1|p \implies q}}
{{Assumption|2|p \lor r}}
{{Commutation|3|2|r \lor p|2|Disjunction}}
{{SequentIntro|4|1|\paren {r \lor p} \implies \paren {r \lor q}|1|Factor Principles/Disjunction on Left/Formulation 1}}
{{ModusPonens|5|1,2|r \lor q|4|3}}
{{Commutation|6|1,2|q \lor r|5|Disjunction}}
{{Implication|7|1|\paren {p \lor r} \implies \paren {q \lor r}|2|6}}
{{EndTableau}}
{{qed}}
Theorem: Factor Principles/Disjunction on Right/Formulation 1

:$p \implies q \vdash \paren {p \lor r} \implies \paren {q \lor r}$

Proof:
As can be seen for all boolean interpretations by inspection, where the truth value under the main connective on the {{LHS}} is $T$, that under the one on the {{RHS}} is also $T$:
:$\begin{array}{|ccc||ccc||ccccccc|} \hline
p & q & r & (p & \implies & q) & (p & \lor & r) & \implies & (q & \lor & r) \\
\hline
F & F & F & F & T & F & F & F & F & T & F & F & F \\
F & F & T & F & T & F & F & T & T & T & F & T & T \\ 
F & T & F & F & T & T & F & F & F & T & T & T & F \\
F & T & T & F & T & T & F & T & T & T & T & T & T \\
T & F & F & T & F & F & T & T & F & F & F & F & F \\
T & F & T & T & F & F & T & T & T & T & F & T & T \\
T & T & F & T & T & T & T & T & F & T & T & T & F \\
T & T & T & T & T & T & T & T & T & T & T & T & T \\
\hline
\end{array}$
{{qed}}
Theorem: Factor Principles/Disjunction on Left/Formulation 1

: $p \implies q \vdash \paren {r \lor p} \implies \paren {r \lor q}$

Proof:
{{BeginTableau|p \implies q \vdash \paren {r \lor p} \implies \paren {r \lor q} }}
{{Premise|1|p \implies q}}
{{TheoremIntro|2|r \implies r|Law of Identity: Formulation 2}}
{{SequentIntro|3|1|\paren {r \lor p} \implies \paren {r \lor q}|2, 1|Constructive Dilemma}}
{{EndTableau}}
{{qed}}
Theorem: Factor Principles/Disjunction on Left/Formulation 1

: $p \implies q \vdash \paren {r \lor p} \implies \paren {r \lor q}$

Proof:
{{BeginTableau|p \implies q \vdash \paren {r \lor p} \implies \paren {r \lor q} }}
{{Premise|1|p \implies q}}
{{Assumption|2|r \lor p}}
{{Assumption|3|r}}
{{Addition|4|3|r \lor q|3|1}}
{{Assumption|5|p}}
{{ModusPonens|6|1, 5|q|1|5}}
{{Addition|7|1, 5|r \lor q|6|2}}
{{ProofByCases|8|1, 2|r \lor q|2|3|4|5|6}}
{{Implication|9|1|\paren {r \lor p} \implies \paren {r \lor q}|2|7}}
{{EndTableau}}
{{qed}}
Theorem: Disjunction of Conditionals

:$\vdash \paren {p \implies q} \lor \paren {q \implies r}$

Proof:
{{BeginTableau|\vdash \paren {p \implies q} \lor \paren {q \implies r} }}
{{ExcludedMiddle|1|q \lor \neg q}}
{{Assumption|2|q}}
{{SequentIntro|3|2|p \implies q|2|True Statement is implied by Every Statement}}
{{Addition|4|2|\paren {p \implies q} \lor \paren {q \implies r}|3|1}}
{{Assumption|5|\neg q}}
{{SequentIntro|6|5|q \implies r|5|False Statement implies Every Statement}}
{{Addition|7|5|\paren {p \implies q} \lor \paren {q \implies r}|6|2}}
{{ProofByCases|8||\paren {p \implies q} \lor \paren {q \implies r}|1|2|4|5|7}}
{{EndTableau|qed}}
{{LEM}}
Theorem: Principle of Composition/Formulation 1/Forward Implication

:$\paren {p \implies r} \lor \paren {q \implies r} \vdash \paren {p \land q} \implies r$

Proof:
{{BeginTableau|\paren {p \implies r} \lor \paren {q \implies r} \vdash \paren {p \land q} \implies r}}
{{Premise        |  1 | \paren {p \implies r} \lor \paren {q \implies r} }}
{{Assumption     |  2 | p \implies r}}
{{Assumption     |  3 | p \land q}}
{{Simplification |  4 | 3 | p | 3 | 1}}
{{ModusPonens    |  5 | 2, 3 | r | 2 | 4}}
{{Implication    |  6 | 2 | \paren {p \land q} \implies r | 3 | 5}}
{{Assumption     |  7 | q \implies r}}
{{Assumption     |  8 | p \land q}}
{{Simplification |  9 | 8 | q | 8 | 2}}
{{ModusPonens    | 10 | 7, 8 | r | 7 | 9}}
{{Implication    | 11 | 7 | \paren {p \land q} \implies r | 8 | 10}}
{{ProofByCases   | 12 | 1 | \paren {p \land q} \implies r | 1 | 2 | 6 | 7 | 11}}
{{EndTableau}}
{{qed}}
Category:Principle of Composition
s0zw4mvifgwuf9geznf0ccfqcepe05p
Theorem: Principle of Composition/Formulation 1/Reverse Implication

:$\paren {p \land q} \implies r \vdash \paren {p \implies r} \lor \paren {q \implies r}$

Proof:
{{BeginTableau|\paren {p \land q} \implies r \vdash \paren {p \implies r} \lor \paren {q \implies r} }}
{{Premise        |  1 | \paren {p \land q} \implies r}}
{{SequentIntro   |  2 | 1 | \neg \paren {p \lor q} \lor r | 1 | Rule of Material Implication}}
{{SequentIntro   |  3 | 1 | \neg p \lor \neg q \lor r | 2 | De Morgan's Laws: Disjunction of Negations}}
{{Addition       |  4 | 1 | r \lor \neg p \lor \neg q \lor r | 3 | 2}}
{{Commutation    |  5 | 1 | \neg p \lor r \lor \neg q \lor r | 4 | Disjunction}}
{{SequentIntro   |  6 | 1 | \paren {p \implies r} \lor \neg q \lor r | 5 | Rule of Material Implication}}
{{SequentIntro   |  7 | 1 | \paren {p \implies r} \lor \paren {q \implies r} | 6 | Rule of Material Implication}}
{{EndTableau}}
{{qed}}
Category:Principle of Composition
lrbsgl53wcyrryvmzb11mbkzydx5lg1
Theorem: Principle of Composition/Formulation 2

:$\paren {\paren {p \implies r} \lor \paren {q \implies r} } \iff \paren {\paren {p \land q} \implies r}$

Proof:
{{BeginTableau|\paren {\paren {p \implies r} \lor \paren {q \implies r} } \iff \paren {\paren {p \land q} \implies r} }}
{{Assumption  |1|\paren {p \implies r} \lor \paren {q \implies r} }}
{{SequentIntro|2|1|\paren {p \land q} \implies r|1|Principle of Composition: Formulation 1}}
{{Implication |3||\paren {\paren {p \implies r} \lor \paren {q \implies r} } \implies \paren {\paren {p \land q} \implies r}|1|2}}
{{Assumption  |4|\paren {p \implies r} \lor \paren {q \implies r} }}
{{SequentIntro|5|4|\paren {p \land q} \implies r|4|Principle of Composition: Formulation 1}}
{{Implication |6||\paren {\paren {p \land q} \implies r} \implies \paren {\paren {p \implies r} \lor \paren {q \implies r} }|4|5}}
{{BiconditionalIntro|7||\paren {\paren {p \implies r} \lor \paren {q \implies r} } \iff \paren {\paren {p \land q} \implies r}|3|6}}
{{EndTableau}}
{{qed}}
Theorem: Inversion Mapping on Topological Group is Homeomorphism

Let $T = \struct {G, \circ, \tau}$ be a topological group.
Let $\phi: G \to G$ be the inversion mapping of $T$.
Then $\phi$ is a homeomorphism.

Proof:
From the definition of topological group, $\phi$ is continuous.
By Inversion Mapping is Involution, $\phi$ is an involution.
By Continuous Involution is Homeomorphism, $\phi$ is a homeomorphism.
{{qed}}
Category:Inversion Mappings
Category:Homeomorphisms (Topological Spaces)
Category:Topological Groups
dd53003fsqyn6lrlf3r9v1107n8a40m
Theorem: De Morgan's Laws (Logic)/Conjunction of Negations/Formulation 2/Forward Implication

:$\paren {\neg p \land \neg q} \implies \paren {\neg \paren {p \lor q} }$

Proof:
{{BeginTableau|\paren {\neg p \land \neg q} \implies \paren {\neg \paren {p \lor q} } }}
{{Assumption|1|\neg p \land \neg q}}
{{SequentIntro|2|1|\neg \paren {p \lor q}|1|De Morgan's Laws (Logic): Conjunction of Negations: Formulation 1}}
{{Implication|3||\paren {\neg p \land \neg q} \implies \paren {\neg \paren {p \lor q} }|1|2}}
{{EndTableau|qed}}
Theorem: De Morgan's Laws (Logic)/Conjunction of Negations/Formulation 2/Reverse Implication

:$\paren {\neg \paren {p \lor q} } \implies \paren {\neg p \land \neg q}$

Proof:
{{BeginTableau|\vdash \paren {\neg \paren {p \lor q} } \implies \paren {\neg p \land \neg q} }}
{{Assumption|1|\neg \paren {p \lor q} }}
{{SequentIntro|2|1|\neg p \land \neg q|1|De Morgan's Laws (Logic): Conjunction of Negations: Formulation 1}}
{{Implication|3||\paren {\neg \paren {p \lor q} } \implies \paren {\neg p \land \neg q}|1|2}}
{{EndTableau|qed}}
Category:De Morgan's Laws (Logic)
1sz1rsl7gaob4g7v3hiiqttc5hfdm88
Theorem: Equivalence of Definitions of Generalized Ordered Space

Let $\struct {S, \preceq}$ be a totally ordered set.
Let $\tau$ be a topology for $S$.
{{TFAE|def = Generalized Ordered Space}}

Proof:
=== Definition $(1)$ implies Definition $(3)$ ===
{{:Equivalence of Definitions of Generalized Ordered Space/Definition 1 implies Definition 3}}{{qed|lemma}}
Theorem: Equivalence of Definitions of Generalized Ordered Space/Definition 2 implies Definition 1

Let $\struct {S, \preceq, \tau}$ be a generalized ordered space by Definition 2:
{{:Definition:Generalized Ordered Space/Definition 2}}
Then $\struct {S, \preceq, \tau}$ is a generalized ordered space by Definition 1:
{{:Definition:Generalized Ordered Space/Definition 1}}

Proof:
Let $x \in U \in \tau$.
Then by the definition of topological embedding:
:$\map \phi U$ is an open neighborhood of $\map \phi x$ in $\map \phi S$ with the subspace topology.
Thus by Basis for Topological Subspace and the definition of the order topology, there is an open interval or open ray $I' \in \tau'$ such that:
:$\map \phi x \in I' \cap \map \phi S \subseteq \map \phi U$
Since $I'$ is an interval or ray, it is order-convex in $S'$ by Interval of Totally Ordered Set is Order-Convex or Ray is Order-Convex, respectively.
Then:
{{begin-eqn}}
{{eqn | l = x \in \phi^{-1} \sqbrk {I'}
      | r = \phi^{-1} \sqbrk {I' \cap \phi \sqbrk S}
      | c = 
}}
{{eqn | o = \subseteq
      | r = \phi^{-1} \sqbrk {\phi \sqbrk U}
      | c = 
}}
{{end-eqn}}
Because $\phi$ is a topological embedding, it is injective by definition.
So:
:$\phi^{-1} \sqbrk {\phi \sqbrk U} = U$
Thus:
:$x \in \phi^{-1} \sqbrk {I'} \subseteq U$
By Inverse Image of Order-Convex Set under Monotone Mapping is Order-Convex:
:$\phi^{-1} \sqbrk {I'}$ is order-convex.
Thus $\tau$ has a basis consisting of order-convex sets.
Theorem: Inverse Image of Order-Convex Set under Monotone Mapping is Order-Convex

Let $\struct {X, \le}$ and $\struct {Y, \preceq}$ be ordered sets.
Let $f: X \to Y$ be a monotone mapping.
Let $C$ be a order-convex subset of $Y$.
Then $f^{-1} \sqbrk C$ is order-convex in $X$.

Proof:
Suppose $f$ is increasing.
Let $a, b, c \in X$ such that $a \le b \le c$.
Let $a, c \in f^{-1} \sqbrk C$.
By definition of inverse image:
:$\map f a, \map f c \in C$
By definition of increasing mapping:
:$\map f a \preceq \map f b \preceq \map f c$
Thus by definition of order-convex set:
:$\map f b \in C$
Then by definition of inverse image:
:$b \in f^{-1} \sqbrk C$
Since this holds for all such triples, $f^{-1} \sqbrk C$ is order-convex in $X$.
A similar argument applies if $f$ is decreasing.
{{qed}}
Category:Order Theory
6i26xnrjod6bq3pm1qru0utmfvxcb9l
Theorem: Conjunction with Law of Excluded Middle

:$\vdash p \iff \paren {p \land q} \lor \paren {p \land \neg q}$

Proof:
{{BeginTableau|\vdash p \iff \paren {p \land q} \lor \paren {p \land \neg q} }}
{{Assumption|1|p}}
{{ExcludedMiddle|2|q \lor \neg q}}
{{Assumption|3|q}}
{{Conjunction|4|1, 3|p \land q|1|2}}
{{Addition|5|1, 3|\paren {p \land q} \lor \paren {p \land \neg q}|4|1}}
{{Assumption|6|\neg q}}
{{Conjunction|7|1, 6|p \land \neg q|1|6}}
{{Addition|8|1, 6|\paren {p \land q} \lor \paren {p \land \neg q}|7|2}}
{{ProofByCases|9|1|\paren {p \land q} \lor \paren {p \land \neg q}|2|3|5|6|8}}
{{Implication|10||p \implies \paren {p \land q} \lor \paren {p \land \neg q}|1|9}}
{{Assumption|11|\paren {p \land q} \lor \paren {p \land \neg q} }}
{{SequentIntro|12|11|p \land \paren {q \lor \neg q}|11|Conjunction Distributes over Disjunction}}
{{Simplification|13|11|p|11|2}}
{{Implication|14||\paren {p \land q} \lor \paren {p \land \neg q} \implies p|11|13}}
{{BiconditionalIntro|15||p \iff \paren {p \land q} \lor \paren {p \land \neg q}|12|14}}
{{EndTableau}}
{{qed}}
Theorem: Proof by Cases with Contradiction

:$\vdash p \iff \paren {p \lor q} \land \paren {p \lor \neg q}$

Proof:
{{BeginTableau|\vdash p \iff \paren {p \lor q} \land \paren {p \lor \neg q} }}
{{Assumption|1|p}}
{{Addition|2|1|p \lor q|1|1}}
{{Addition|3|1|p \lor \neg q|1|2}}
{{Conjunction|4|1|\paren {p \lor q} \land \paren {p \lor \neg q} |2|3}}
{{Implication|5||p \implies \paren {p \lor q} \land \paren {p \lor \neg q}|1|4}}
{{Assumption|6|\paren {p \lor q} \land \paren {p \lor \neg q} }}
{{SequentIntro|7|6|p \lor \paren {q \land \neg q}|6|Disjunction Distributes over Conjunction}}
{{Assumption|8|p}}
{{TheoremIntro|9|\map \neg {q \land \neg q}|Principle of Non-Contradiction: Formulation 2}}
{{ModusTollendoPonens|10|6|p|7|9|2}}
{{ProofByCases|11|6|p|6|8|8|9|10}}
{{Implication|12||\paren {p \lor q} \land \paren {p \lor \neg q} \implies p|6|11}}
{{BiconditionalIntro|13||p \iff \paren {p \lor q} \land \paren {p \lor \neg q}|5|12}}
{{EndTableau}}
{{qed}}