avewright/proofwiki-math huggingface dataset:
Theorem: Biconditional is Commutative/Formulation 1/Proof 1

: $p \iff q \dashv \vdash q \iff p$

Proof:
{{BeginTableau|p \iff q \vdash q \iff p}}
{{Premise|1|p \iff q}}
{{BiconditionalElimination|2|1|p \implies q|1|1}}
{{BiconditionalElimination|3|1|q \implies p|1|2}}
{{BiconditionalIntro|4|1|q \iff p|3|2}}
{{EndTableau}}
{{qed|lemma}}
{{BeginTableau|q \iff p \vdash p \iff q}}
{{Premise|1|q \iff p}}
{{BiconditionalElimination|2|1|q \implies p|1|1}}
{{BiconditionalElimination|3|1|p \implies q|1|2}}
{{BiconditionalIntro|4|1|p \iff q|3|2}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Material Equivalence/Formulation 1

:$p \iff q \dashv \vdash \paren {p \implies q} \land \paren {q \implies p}$

Proof:
{{BeginTableau|p \iff q \vdash \paren {p \implies q} \land \paren {q \implies p} }}
{{Premise|1|p \iff q}}
{{BiconditionalElimination|2|1|p \implies q|1|1}}
{{BiconditionalElimination|3|1|q \implies p|1|2}}
{{Conjunction|4|1|\paren {p \implies q} \land \paren {q \implies p}|2|3}}
{{EndTableau}}
{{BeginTableau|\paren {p \implies q} \land \paren {q \implies p} \vdash p \iff q}}
{{Premise|1|\paren {p \implies q} \land \paren {q \implies p} }}
{{Simplification|2|1|p \implies q|1|1}}
{{Simplification|3|1|q \implies p|1|2}}
{{BiconditionalIntro|4|1|p \iff q|2|3}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Material Equivalence/Formulation 1

:$p \iff q \dashv \vdash \paren {p \implies q} \land \paren {q \implies p}$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
:<nowiki>$\begin{array}{|ccc|ccccccc|} \hline
p & \iff & q & (p & \implies & q) & \land & (q & \implies & p) \\
\hline
\F & \T & \F & \F & \T & \F & \T & \F & \T & \F \\
\F & \F & \T & \F & \T & \T & \F & \T & \F & \F \\
\T & \F & \F & \T & \F & \F & \F & \F & \T & \T \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Equivalences are Interderivable/Forward Implication

: $\left ({p \dashv \vdash q}\right) \vdash \left ({p \iff q}\right)$

Proof:
{{BeginTableau|\left({p \dashv \vdash q}\right) \vdash p \iff q}}
{{Premise|1|p \dashv \vdash q}}
{{SequentIntro|2|1|\left ({p \vdash q}\right) \land \left ({q \vdash p}\right)|1
  |Definition of Interderivable}}
{{Assumption|3|p}}
{{Simplification|4|1, 3|p \vdash q|2|1}}
{{Implication|5|1|p \implies q|3|4}}
{{Assumption|6|q}}
{{Simplification|7|1, 6|q \vdash p|2|2}}
{{Implication|8|1|q \implies p|6|7}}
{{BiconditionalIntro|9|1|p \iff q|5|8}}
{{EndTableau}}
{{Qed}}
Category:Equivalences are Interderivable
s1qqzy938u5n0099qdwkh50zrgg4tkc
Theorem: Equivalences are Interderivable/Reverse Implication

: $\left ({p \iff q}\right) \vdash \left ({p \dashv \vdash q}\right)$

Proof:
{{BeginTableau|p \iff q \vdash \left({p \vdash q}\right)}}
{{Premise|1|p \iff q}}
{{BiconditionalElimination|3|1|p \implies q|1|1}}
{{Assumption|3|p}}
{{ModusPonens|4|1, 3|q|2|3}}
{{EndTableau}}
{{qed|lemma}}
{{BeginTableau|p \iff q \vdash \left({q \vdash p}\right)}}
{{Premise|1|p \iff q}}
{{BiconditionalElimination|3|1|p \implies q|1|2}}
{{Assumption|3|q}}
{{ModusPonens|4|1, 3|p|2|3}}
{{EndTableau}}
{{qed}}
Category:Equivalences are Interderivable
mdne6teoypnkvrjoq2gr6rw5bg536yu
Theorem: Compact Subspace of Linearly Ordered Space/Reverse Implication

Let $\struct {X, \preceq, \tau}$ be a linearly ordered space.
Let $Y \subseteq X$ be a non-empty subset of $X$.
Let the following hold:
:$(1): \quad$ For every non-empty $S \subseteq Y$, $S$ has a supremum and an infimum in $X$.
:$(2): \quad$ For every non-empty $S \subseteq Y$: $\sup S, \inf S \in Y$.
Then $Y$ is a compact subspace of $\struct {X, \tau}$.

Proof:
Let $\tau'$ be the $\tau$-relative subspace topology on $Y$.
Let $\preceq'$ be the restriction of $\preceq$ to $Y$.
=== Lemma ===
{{:Compact Subspace of Linearly Ordered Space/Lemma 2}}{{qed|lemma}}
The premises immediately show that $\struct {Y, \preceq'}$ is a complete lattice.
By Complete Linearly Ordered Space is Compact, $Y$ is a compact subspace of $X$.
{{qed}}
Theorem: Compact Subspace of Linearly Ordered Space/Reverse Implication

Let $\struct {X, \preceq, \tau}$ be a linearly ordered space.
Let $Y \subseteq X$ be a non-empty subset of $X$.
Let the following hold:
:$(1): \quad$ For every non-empty $S \subseteq Y$, $S$ has a supremum and an infimum in $X$.
:$(2): \quad$ For every non-empty $S \subseteq Y$: $\sup S, \inf S \in Y$.
Then $Y$ is a compact subspace of $\struct {X, \tau}$.

Proof:
Let $\FF$ be an ultrafilter on $Y$.
For $S \in \FF$, let $\map f S = \inf S$.
Let $p = \sup \map f \FF$.
{{improve|perhaps directly use $p :{{=}} \ds \sup_{S \mathop \in \FF} \inf S$?}}
Then $\FF$ converges to $p$:
=== Upward rays ===
Let $a \in X$ with $a \prec p$.
Since $\FF$ is an ultrafilter, either $Y \cap {\uparrow} a \in \FF$ or $Y \cap {\bar \downarrow} a \in \FF$.
{{AimForCont}} that $Y \cap {\bar \downarrow} a \in \FF$.
For each $S \in \FF$:
:$S \cap {\bar \downarrow} a \in \FF$ because an ultrafilter is a filter.
{{explain|Mention that $S \cap (Y \cap {\bar \downarrow} a) {{=}} S \cap {\bar \downarrow} a$ is used}}
:$S \cap {\bar \downarrow} a \ne \O$ because a filter on a set is proper.
By applying the definition of supremum to $p$, it follows that there exists an $S \in \FF$ such that $a \prec \inf S$.
By the definition of infimum:
:$S \cap {\bar \downarrow} a = \O$
which is a contradiction.
Thus $Y \cap {\uparrow} a \in \FF$.
=== Downward rays ===
Let $b \in X$ with $p \prec b$.
Either $Y \cap {\downarrow} b \in \FF$ or $Y \cap {\bar \uparrow} b \in \FF$.
{{AimForCont}} that $Y \cap {\bar \uparrow} b \in \FF$.
Let $b' = \map \inf {Y \cap {\bar \uparrow} b}$.
We have that $b$ is a lower bound of $Y \cap {\bar \uparrow} b$
So by the definition of infimum:
:$b \preceq b'$
Since $p \prec b$ and $b \preceq b'$, $p \prec b'$ by Extended Transitivity.
By the definition of $b'$ and the definition of $f$:
:$b' \in \map f \FF$
But this contradicts the fact that $p$ is the supremum, and hence an upper bound, of $\map f \FF$.
{{qed|lemma}}
By the definition of the order topology, the upward and downward rays containing each point form a neighborhood sub-basis for that point.
{{wtd|an invocation of "Sub-Basis is Nbhd Sub-Basis" would be appropriate}}
Thus by the Neighborhood Sub-Basis Criterion for Filter Convergence, $\FF$ converges.
Since every ultrafilter on $Y$ converges, $Y$ is compact by Equivalence of Definitions of Compact Topological Space.
Theorem: Modus Ponendo Tollens/Sequent Form/Case 1

:$\neg \paren {p \land q}, p \vdash \neg q$

Proof:
{{BeginTableau|\neg \paren {p \land q}, p \vdash \neg q}}
{{Premise|1|\neg \paren {p \land q} }}
{{Premise|2|p}}
{{Assumption|3|q}}
{{Conjunction|4|2, 3|p \land q|2|3}}
{{NonContradiction|5|1, 2, 3|4|1}}
{{Contradiction|6|1, 2|\neg q|3|5}}
{{EndTableau|qed}}
Theorem: Modus Ponendo Tollens/Sequent Form/Case 2

:$\neg \left({p \land q}\right), q \vdash \neg p$

Proof:
{{BeginTableau|\neg \left({p \land q}\right), q \vdash \neg p}}
{{Premise|1|\neg \left({p \land q}\right)}}
{{Premise|2|q}}
{{Assumption|3|p}}
{{Conjunction|4|2, 3|p \land q|3|2}}
{{NonContradiction|5|1, 2, 3|4|1}}
{{Contradiction|6|1, 2|\neg p|3|5}}
{{EndTableau}}
{{qed}}
Category:Modus Ponendo Tollens
mjeey35ngrumpe26ifn1ui05rzz2i9e
Theorem: Union of Subsets is Subset/Subset of Power Set

Let $S$ and $T$ be sets.
Let $\powerset S$ be the power set of $S$.
Let $\mathbb S$ be a subset of $\powerset S$.
Then:
:$\ds \paren {\forall X \in \mathbb S: X \subseteq T} \implies \bigcup \mathbb S \subseteq T$

Proof:
Let $\mathbb S \subseteq \powerset S$.
Suppose that $\forall X \in \mathbb S: X \subseteq T$.
Consider any $\ds x \in \bigcup \mathbb S$.
By definition of set union, it follows that:
:$\exists X \in \mathbb S: x \in X$
But as $X \subseteq T$ it follows that $x \in T$.
Thus it follows that:
:$\ds \bigcup \mathbb S \subseteq T$
So:
:$\ds \paren {\forall X \in \mathbb S: X \subseteq T} \implies \bigcup \mathbb S \subseteq T$
{{qed}}
Category:Set Union
Category:Subsets
sqbcr2yehljqbrorrxy6i6707wvbk2j
Theorem: Conjunction with Negative is Equivalent to Negation of Conditional/Formulation 2/Forward Implication

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

Proof:
{{BeginTableau|\vdash \paren {p \land \neg q} \implies \paren {\neg \paren {p \implies q} } }}
{{Assumption|1|p \land \neg q}}
{{Assumption|2|p \implies q| Assume the opposite of what is to be proved ...}}
{{Simplification|3|1|p|1|1}}
{{Simplification|4|1|\neg q|1|2}}
{{ModusPonens|5|1, 2|q|2|3}}
{{NonContradiction|6|1, 2|5|4|... and demonstrate a contradiction}}
{{Contradiction|7|1|\neg \paren {p \implies q}|2|6}}
{{Implication|3||\paren {p \land \neg q} \implies \paren {\neg \paren {p \implies q} }|1|2}}
{{EndTableau|qed}}
Theorem: Conjunction with Negative is Equivalent to Negation of Conditional/Formulation 2/Reverse Implication

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

Proof:
{{BeginTableau|\vdash \paren {\neg \paren {p \implies q} } \implies \paren {p \land \neg q} }}
{{Assumption|1|\neg \paren {p \implies q} }}
{{Assumption|2|\neg \paren {p \land \neg q} }}
{{SequentIntro|3|2|p \implies q|2|Conditional is Equivalent to Negation of Conjunction with Negative}}
{{NonContradiction|4|1, 2|3|1}}
{{Reductio|5|1|p \land \neg q|2|4}}
{{Implication|6||\paren {\neg \paren {p \implies q} } \implies \paren {p \land \neg q}|1|5}}
{{EndTableau|qed}}
{{LEM|Reductio ad Absurdum|3}}
Theorem: Conjunction with Negative is Equivalent to Negation of Conditional/Formulation 2/Reverse Implication

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

Proof:
{{BeginTableau|\vdash \paren {\neg \paren {p \implies q} } \implies \paren {p \land \neg q} }}
{{Assumption|1|\neg \paren {p \implies q} }}
{{SequentIntro|2|1|p \land \neg q|1|Conjunction with Negative is Equivalent to Negation of Conditional: Formulation 1: Reverse Implication}}
{{Implication|3||\paren {\neg \paren {p \implies q} } \implies \paren {p \land \neg q}|1|2}}
{{EndTableau|qed}}
{{LEM|Conjunction with Negative is Equivalent to Negation of Conditional/Formulation 1/Reverse Implication|3}}
Theorem: Convex Set is Star Convex Set

Let $V$ be a vector space over $\R$ or $\C$.
Let $A \subseteq V$ be a non-empty convex set.
Then $A$ is a star convex set, and every point in $A$ is a star center.

Proof:
Let $a \in A$.
Note that there is at least one point in $A$, as $A$ is non-empty.
If $x \in A$, then there is a line segment joining $a$ and $x$.
By definition, it follows that $A$ is star convex, and $a$ is a star center.
{{qed}}
Category:Convex Sets (Vector Spaces)
bnnv4ei5bq7etdgcg2soj8upxict53j
Theorem: Negation implies Negation of Conjunction/Case 1

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

Proof:
{{BeginTableau|\neg p \implies \neg \paren {p \land q} }}
{{Assumption|1|\neg p}}
{{Assumption|2|p \land q}}
{{Simplification|3|2|p|2|1}}
{{NonContradiction|4|1, 2|3|1}}
{{Contradiction|5|1|\neg \paren {p \land q}|2|4}}
{{Implication|6||\neg p \implies \neg \paren {p \land q}|1|5}}
{{EndTableau|qed}}
Theorem: Negation implies Negation of Conjunction/Case 2

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

Proof:
{{BeginTableau|\neg q \implies \neg \paren {p \land q} }}
{{Assumption|1|\neg q}}
{{Assumption|2|p \land q}}
{{Simplification|3|2|q|2|2}}
{{NonContradiction|4|1, 2|3|1}}
{{Contradiction|5|1|\neg \paren {p \land q}|2|4}}
{{Implication|6||\neg q \implies \neg \paren {p \land q}|1|5}}
{{EndTableau|qed}}
Theorem: Neighborhood Sub-Basis Criterion for Filter Convergence

Let $\struct {S, \tau}$ be a topological space.
Let $\FF$ be a filter on $S$.
Let $p \in S$.
Then $\FF$ converges to $p$ {{iff}} $\FF$ contains as a subset a neighborhood sub-basis at $p$.

Proof:
=== Sufficient Condition ===
Let $\FF$ converges to $p$.
Then it contains ''every'' neighborhood of $p$.
The set of neighborhoods of $p$ is trivially a neighborhood sub-basis at $p$.
{{qed|lemma}}
Theorem: Rule of Material Implication/Formulation 2/Forward Implication

: $\vdash \left({p \implies q}\right) \implies \left({\neg p \lor q}\right)$

Proof:
{{BeginTableau|\left({p \implies q}\right) \implies \left({\neg p \lor q}\right)}}
{{Assumption|1|p \implies q}}
{{SequentIntro|2|1|\neg p \lor q|1|Rule of Material Implication: Formulation 1}}
{{Implication|3||\left({p \implies q}\right) \implies \left({\neg p \lor q}\right)|1|2}}
{{EndTableau}}
{{qed}}
{{LEM|Rule of Material Implication/Formulation 1/Forward Implication|3}}
Theorem: Rule of Material Implication/Formulation 2/Reverse Implication

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

Proof:
{{BeginTableau|\paren {\neg p \lor q} \implies \paren {p \implies q} }}
{{Assumption|1|\neg p \lor q}}
{{SequentIntro|2|1|p \implies q|1|Rule of Material Implication: Formulation 1}}
{{Implication|3||\paren {\neg p \lor q} \implies \paren {p \implies q}|1|2}}
{{EndTableau}}
{{qed}}
Theorem: Compact Subspace of Linearly Ordered Space

Let $\struct {X, \preceq, \tau}$ be a linearly ordered space.
Let $Y \subseteq X$ be a non-empty subset of $X$.
Then $Y$ is a compact subspace of $\struct {X, \tau}$ {{iff}} both of the following hold:
:$(1): \quad$ For every non-empty $S \subseteq Y$, $S$ has a supremum and an infimum in $X$.
:$(2): \quad$ For every non-empty $S \subseteq Y$: $\sup S, \inf S \in Y$.

Proof:
=== Forward Implication ===
Let $S$ be a non-empty subset of $Y$.
By Compact Subspace of Linearly Ordered Space: Lemma 1, $S$ has a supremum $k$ in $Y$.
{{explain|The lemma shows that the structure in question is a complete lattice. Take that further step to assert the existence of the supremum.}}
{{explain|supremum WRT $\preceq \restriction_Y$}}
{{AimForCont}} that $S$ has an upper bound $b$ in $X$ such that $b \prec k$.
Let:
:$\AA = \set {s^\preceq: s \in S} \cup \set {b^\succeq}$
where:
:$s^\preceq$ denotes the lower closure of $s$ in $S$
:$b^\succeq$ denotes the upper closure of $s$ in $S$.
Then $\AA$ is an open cover of $Y$.
But $\AA$ has no finite subcover, contradicting the fact that $Y$ is compact.
{{finish|above lines need proof}}
{{explain|Pronounce proper incantations about duality.}}
A similar argument proves the corresponding statement for infima, so $(2)$ holds.
{{qed|lemma}}
Theorem: Compact Subspace of Linearly Ordered Space

Let $\struct {X, \preceq, \tau}$ be a linearly ordered space.
Let $Y \subseteq X$ be a non-empty subset of $X$.
Then $Y$ is a compact subspace of $\struct {X, \tau}$ {{iff}} both of the following hold:
:$(1): \quad$ For every non-empty $S \subseteq Y$, $S$ has a supremum and an infimum in $X$.
:$(2): \quad$ For every non-empty $S \subseteq Y$: $\sup S, \inf S \in Y$.

Proof:
Let $\tau'$ be the $\tau$-relative subspace topology on $Y$.
Let $\preceq'$ be the restriction of $\preceq$ to $Y$.
=== Lemma ===
{{:Compact Subspace of Linearly Ordered Space/Lemma 2}}{{qed|lemma}}
The premises immediately show that $\struct {Y, \preceq'}$ is a complete lattice.
By Complete Linearly Ordered Space is Compact, $Y$ is a compact subspace of $X$.
{{qed}}
Theorem: Compact Subspace of Linearly Ordered Space

Let $\struct {X, \preceq, \tau}$ be a linearly ordered space.
Let $Y \subseteq X$ be a non-empty subset of $X$.
Then $Y$ is a compact subspace of $\struct {X, \tau}$ {{iff}} both of the following hold:
:$(1): \quad$ For every non-empty $S \subseteq Y$, $S$ has a supremum and an infimum in $X$.
:$(2): \quad$ For every non-empty $S \subseteq Y$: $\sup S, \inf S \in Y$.

Proof:
Let $\FF$ be an ultrafilter on $Y$.
For $S \in \FF$, let $\map f S = \inf S$.
Let $p = \sup \map f \FF$.
{{improve|perhaps directly use $p :{{=}} \ds \sup_{S \mathop \in \FF} \inf S$?}}
Then $\FF$ converges to $p$:
=== Upward rays ===
Let $a \in X$ with $a \prec p$.
Since $\FF$ is an ultrafilter, either $Y \cap {\uparrow} a \in \FF$ or $Y \cap {\bar \downarrow} a \in \FF$.
{{AimForCont}} that $Y \cap {\bar \downarrow} a \in \FF$.
For each $S \in \FF$:
:$S \cap {\bar \downarrow} a \in \FF$ because an ultrafilter is a filter.
{{explain|Mention that $S \cap (Y \cap {\bar \downarrow} a) {{=}} S \cap {\bar \downarrow} a$ is used}}
:$S \cap {\bar \downarrow} a \ne \O$ because a filter on a set is proper.
By applying the definition of supremum to $p$, it follows that there exists an $S \in \FF$ such that $a \prec \inf S$.
By the definition of infimum:
:$S \cap {\bar \downarrow} a = \O$
which is a contradiction.
Thus $Y \cap {\uparrow} a \in \FF$.
=== Downward rays ===
Let $b \in X$ with $p \prec b$.
Either $Y \cap {\downarrow} b \in \FF$ or $Y \cap {\bar \uparrow} b \in \FF$.
{{AimForCont}} that $Y \cap {\bar \uparrow} b \in \FF$.
Let $b' = \map \inf {Y \cap {\bar \uparrow} b}$.
We have that $b$ is a lower bound of $Y \cap {\bar \uparrow} b$
So by the definition of infimum:
:$b \preceq b'$
Since $p \prec b$ and $b \preceq b'$, $p \prec b'$ by Extended Transitivity.
By the definition of $b'$ and the definition of $f$:
:$b' \in \map f \FF$
But this contradicts the fact that $p$ is the supremum, and hence an upper bound, of $\map f \FF$.
{{qed|lemma}}
By the definition of the order topology, the upward and downward rays containing each point form a neighborhood sub-basis for that point.
{{wtd|an invocation of "Sub-Basis is Nbhd Sub-Basis" would be appropriate}}
Thus by the Neighborhood Sub-Basis Criterion for Filter Convergence, $\FF$ converges.
Since every ultrafilter on $Y$ converges, $Y$ is compact by Equivalence of Definitions of Compact Topological Space.
Theorem: Linearly Ordered Space is Hausdorff

Let $\struct {X, \preceq, \tau}$ be a linearly ordered space.
Then $\struct {X, \tau}$ is a Hausdorff space.

Proof:
Let $x, y \in X$ with $x \ne y$.
Since $\le$ is a total ordering, either $x \prec y$ or $y \prec x$.
{{WLOG}}, assume that $x \prec y$.
If there is a $z \in X$ such that $x \prec z \prec y$, then $z^\prec$ and $z^\succ$ separate $x$ and $y$.
Otherwise, by Upper Closure is Strict Upper Closure of Immediate Predecessor, $y^\prec$ and $x^\succ$ separate $x$ and $y$.
Since any two distinct points can be separated by neighborhoods, $\struct {X, \tau}$ is a Hausdorff space.
{{qed}}
Category:Linearly Ordered Spaces
Category:Examples of Hausdorff Spaces
jclowu0wd3t6ver9m4jc1kztmii1pyo
Theorem: Subset of Linearly Ordered Space which is Order-Complete and Closed but not Compact

Let $X = \hointr 0 1 \cup \openint 2 3 \cup \set 4$.
Let $\preceq$ be the ordering on $X$ induced by the usual ordering of the real numbers.
Let $\tau$ be the $\preceq$ order topology on $X$.
Let $Y = \hointr 0 1 \cup \set 4$.
Let $\tau'$ be the $\tau$-relative subspace topology on $Y$.
Then:
:$\struct {Y, \preceq}$ is a complete lattice
:$Y$ is closed in $X$
but:
:$\struct {Y, \tau'}$ is not compact.

Proof:
First it is demonstrated that $\struct {Y, \preceq}$ is a complete lattice.
Let $\phi: Y \to \closedint 0 1$ be defined as:
:<nowiki>$\map \phi y = \begin{cases}
y & : y \in \hointr 0 1 \\
1 & : y = 4 \end{cases}$</nowiki>
Then $\phi$ is a order isomorphism.
{{explain|The above needs to be proved.}}
{{qed|lemma}}
We have that $\closedint 0 1$ is a complete lattice.
{{explain|This is probably around here somewhere.}}
Next is is shown that $\struct {Y, \preceq}$ is closed in $X$.
Let $x \in X \setminus Y$.
Then:
:$x \in \openint 2 3$
Thus:
:$x \in \openint {\dfrac {x + 2} 2} {\dfrac {x + 3} 2} \in \tau'$
Since the complement of $Y$ is open, $Y$ is closed.
Finally it is shown that $\struct {Y, \tau'}$ is not compact.
Let:
:$\AA = \set {x^\preceq: x \in \hointr 0 1} \cup \set {\paren {\dfrac 5 2}^\succeq}$
where:
:$x^\preceq$ denotes the lower closure of $x$
:$x^\succeq$ denotes the upper closure of $x$
Then $\AA$ is an open cover of $Y$ with no finite subcover.
{{explain|Prove the above statement.}}
{{qed}}
{{finish|The remaining parts of this proof need to be completed.}}
Category:Order Topologies
5wotq330daqew0iuet382zog6k2jfn4
Theorem: Rule of Explosion/Variant 2

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

Proof:
{{BeginTableau|\vdash \paren {p \land \neg p} \implies q}}
{{Assumption|1|p \land \neg p}}
{{Simplification|2|1|p|1|1}}
{{Simplification|3|1|\neg p|1|2}}
{{Addition|4|1|p \lor q|2|1}}
{{ModusTollendoPonens|5|1|q|4|3}}
{{EndTableau|qed}}
Theorem: Jordan Curve Theorem

Let $\gamma: \closedint 0 1 \to \R^2$ be a Jordan curve.
Let $\Img \gamma$ denote the image of $\gamma$.
Then $\R^2 \setminus \Img \gamma$ is a union of two disjoint connected components.
Both components are open in $\R^2$, and both components have $\Img \gamma$ as their boundary.
One component is bounded, and is called the interior of $\gamma$.
The other component is unbounded, and is called the exterior of $\gamma$.

Proof:
{{proof wanted}}
{{Namedfor|Marie Ennemond Camille Jordan|cat = Jordan, C}}
Theorem: Heine-Borel Theorem/Dedekind Complete Space

Let $T = \struct {X, \preceq, \tau}$ be a Dedekind-complete linearly ordered space.
Let $Y$ be a non-empty subset of $X$.
Then $Y$ is compact {{iff}} $Y$ is closed and bounded in $T$.

Proof:
=== Sufficient Condition ===
Let $Y$ be a compact subspace of $T$.
From:
:Linearly Ordered Space is Hausdorff
:Compact Subspace of Hausdorff Space is Closed
it follows that $Y$ is closed in $T$.
From Compact Subspace of Linearly Ordered Space: Lemma 1, $\struct {Y, \preceq {\restriction_Y} }$ is a complete lattice.
{{finish|Not much to do, just need to show that a complete lattice in this context is bounded.}}
Hence $Y$ is closed and bounded in $T$.
Theorem: Heine-Borel iff Dedekind Complete

Let $\struct {X, \preceq, \tau}$ be a linearly ordered space.
Then $X$ is Dedekind complete {{iff}} every closed, bounded subset of $X$ is compact.

Proof:
The forward implication follows from Heine-Borel Theorem: Dedekind-Complete Space.
Suppose that $X$ is not Dedekind complete.
Then $X$ has a non-empty subset $S$ with an upper bound $b$ in $X$ but no supremum in $X$.
Let $a \in S$ and let $Y = {\bar \downarrow} S \cap {\bar \uparrow} a$.
$Y$ is nonempty and bounded below by $a$ and above by $b$.