avewright/proofwiki-math huggingface dataset:
Theorem: Filter Generated by Net Converges iff Net Converges

Let $\struct {X, \tau}$ be a topological space.
Let $\struct {\Lambda, \preceq}$ be a directed set.
Let $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ be a net.
Let $\FF$ be the filter generated by $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$.
Let $x \in X$.
Then $\FF$ converges to $x$ {{iff}} $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ converges to $x$.

Proof:
For each $\lambda_0 \in \Lambda$, set:
:$B_{\lambda_0} = \set {x_\lambda : \lambda_0 \succeq \lambda}$ 
Let $\UU_x$ be the neighborhood filter at $x$.
We have that $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ converges to $x$ {{iff}} for each $U \in \UU_x$, there exists $\lambda_0 \in \Lambda$ such that $B_{\lambda_0} \subseteq U$.
Theorem: Outer Jordan Content of Open Rectangle

Let:
:$\ds R = \prod_{i \mathop = 1}^n \openint {a_i} {b_i}$
be an open $n$-rectangle, where:
:$a_i \le b_i$
for each $i \in \set {1, \dots, n}$.
Then:
:$\ds \map {m^*} R = \prod_{i \mathop = 1}^n \paren {b_i - a_i}$
where $m^*$ denotes the outer Jordan content.

Proof:
By Outer Jordan Content of Closed Rectangle, we know that, for:
:$\ds \overline R = \prod_{i \mathop = 1}^n \closedint {a_i} {b_i}$
the outer Jordan content is:
:$\ds \map {m^*} {\overline R} = \map V {\overline R} = \prod_{i \mathop = 1}^n \paren {b_i} {a_i}$
Let us form the subdivision:
:$P = \tuple {P_1, \dots, P_n}$
where:
:$P_i = \set {a_i, b_i}$
The result follows from Outer Jordan Content of Subdivision.
{{qed}}
Category:Outer Jordan Content
k9yv7cqfm51gv253lgiirdeb0hqfb4i
Theorem: Point is Cluster Point of Net iff Limit of Subnet

Let $\struct {X, \tau}$ be a topological space.
Let $\struct {\Lambda, \preceq}$ be a directed set.
Let $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ be a net.
Let $x \in X$.
Then $x$ is a cluster point of $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ {{iff}}:
:there exists a directed set $\struct {A, \sqsubseteq}$ and an increasing cofinal mapping $\lambda : A \to \Lambda$ such that:
::$\family {x_{\map \phi \alpha} }_{\alpha \mathop \in A}$ is a subnet converging to $x$.

Proof:
For each $x \in X$, let $\UU_x$ be the neighborhood filter at $x$.
Theorem: Product of Preordered Sets is Preordered

Let $\struct {P_1, \preceq_1}$ and $\struct {P_2, \preceq_2}$ be preordered sets.
Let $P = P_1 \times P_2$.
Define the relation $\preceq$ on $P$ by:
:$\tuple {p_1, p_2} \preceq \tuple {q_1, q_2}$ 
for each $\tuple {p_1, p_2}, \tuple {q_1, q_2} \in P$.
{{Explain|What type of preordering is $\preceq$? Create and link to the definition page for product preordering, generalizing Definition:Order Product. Perhaps this page should be split for each product preordering.}}
Then $\preceq$ is a preordering on $P$.

Proof:
=== $\preceq$ is reflexive ===
Let $\tuple {p_1, p_2} \in P$.
Since $\preceq_1$ and $\preceq_2$ are preorderings, we have $p_1 \preceq_1 p_1$ and $p_2 \preceq p_2$.
Hence $\tuple {p_1, p_2} \preceq \tuple {p_1, p_2}$.
Hence $\preceq$ is reflexive.
{{qed|lemma}}
Theorem: Characterization of Compactness in terms of Nets

Let $\struct {X, \tau}$ be a topological space.
Then $X$ is compact {{iff}} every net in $X$ has a convergent subnet.

Proof:
For each $x \in X$, let $\UU_x$ be the neighborhood filter at $x$.
Theorem: Cluster Point of Convergent Net in Hausdorff Space is Limit

Let $\struct {X, \tau}$ be a Hausdorff space.
Let $x \in X$.
Let $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ be a convergent net with limit $x$.
Let $y$ be a cluster point of $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$.
Then $x = y$.

Proof:
{{AimForCont}} that $x \ne y$. 
Since $\struct {X, \tau}$ is Hausdorff space, there exists an open neighborhood $U$ of $x$ and an  open neighborhood $v$ of $y$ such that:
:$U \cap V = \O$
Since $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ converges to $x$, there exists $\lambda_0 \in \Lambda$ such that:
:$x_\lambda \in U$ for $\lambda \succeq \lambda_0$.
Since $y$ is a cluster point of $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$, there exists $\lambda_1 \succeq \lambda_0$ such that:
:$x_{\lambda_1} \in V$
However then $x_{\lambda_1} \in U \cap V = \O$, a contradiction.
Hence $x = y$.
{{qed}}
Category:Convergent Nets
Category:Hausdorff Spaces
bsr741820vhaaipqvt80tiu33lhx01a
Theorem: Weak Cluster Point of Basic Sequence in Banach Space is Zero Vector

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ be a Banach space over $\GF$.
Let $w$ be the weak topology on $\struct {X, \norm {\, \cdot \,}_X}$.
Let $\sequence {x_n}_{n \mathop \in \N}$ be a basic sequence.
Let $x$ be a cluster point of $\sequence {x_n}_{n \mathop \in \N}$ in $\struct {X, w}$.
Then $x = {\mathbf 0}_X$.

Proof:
Let $\sqbrk {x_n}_{n \mathop \in \N}$ be the closed linear span of $\sequence {x_n}_{n \mathop \in \N}$.
Let $\cl_w$ be the closure taken in $\struct {X, w}$. 
Since $x$ is a cluster point of $\sequence {x_n}_{n \mathop \in \N}$ in $\struct {X, w}$:
:there exists a subnet $\family {x_{n_\lambda} }_{\lambda \mathop \in \Lambda}$ converging to $x$
from Point is Cluster Point of Net iff Limit of Subnet.
From Point in Set Closure iff Limit of Net, we have $x \in \map {\cl_w} {\sqbrk {x_n}_{n \mathop \in \N} }$. 
From Linear Subspace is Convex Set, we have that $\sqbrk {x_n}_{n \mathop \in \N}$ is convex.
Hence by Mazur's Theorem, we have $\map {\cl_w} {\sqbrk {x_n}_{n \mathop \in \N} } = \sqbrk {x_n}_{n \mathop \in \N}$.
Hence we have $x \in \sqbrk {x_n}_{n \mathop \in \N}$.
Hence, since $\sequence {x_n}_{n \mathop \in \N}$ is a basic sequence, we have:
:$\ds x = \sum_{n \mathop = 1}^\infty \map {x_n^\ast} x x_n$
where $\sequence {x_n^\ast}_{n \mathop \in \N}$ are the coordinate functionals associated with $\sequence {x_n}_{n \mathop \in \N}$.
Since $\family {x_{n_\lambda} }_{\lambda \mathop \in \Lambda}$ converges to $x$, we have:
:$\map {x_k^\ast} {x_{n_\lambda} } \to \map {x_k^\ast} x$
for each $n \in \N$, from Characterization of Continuity in terms of Nets.
On the other hand, since $\family {n_\lambda}_{\lambda \mathop \in \Lambda}$ is cofinal, there exists $\lambda_0 \in \Lambda$ such that $n_{\lambda_0} \ge k + 1$. 
Then for $\lambda \in \Lambda$ satisfying $\lambda \succeq \lambda_0$, we have $n_\lambda \ge n_{\lambda_0} \ge k + 1$ and hence:
:$\map {x_k^\ast} {x_{n_\lambda} } = \delta_{k n_\lambda} = 0$
Hence $\family {\map {x_k^\ast} {x_\lambda} }_{\lambda \mathop \in \Lambda}$ converges to $0$ for each $k \in \N$.
From Characterization of Hausdorff Property in terms of Nets, we must therefore have:
:$\map {x_k^\ast} x = 0$ for all $k \in \N$.
Hence $x = {\mathbf 0}_X$.
{{qed}}
Theorem: Characterization of Compactness in terms of Nets/Corollary

:$X$ is compact {{iff}} every net in $X$ has a cluster point.

Proof:
From Characterization of Compactness in terms of Nets, we have that:
:$X$ is compact {{iff}} every net in $X$ has a convergent subnet.
From Point is Cluster Point of Net iff Limit of Subnet:
:a point $x$ is a cluster point of a net {{iff}} it is the limit of a convergent subnet.
Hence:
:$X$ compact {{iff}} every net in $X$ has a cluster point.
{{qed}}
Category:Characterization of Compactness in terms of Nets
fll4y170y28262gimzceedd0dqktee3
Theorem: Kadets-Pełczyński Criterion on the Existence of a Basic Sequence

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ be a Banach space over $\GF$.
Let $w$ be the weak topology on $\struct {X, \norm {\, \cdot \,}_X}$.
Let $\cl_w$ be the closure in $\struct {X, w}$.
Let $S \subseteq X$ be such that:
:$\ds 0 < \inf_{x \mathop \in S} \norm x_X \le \sup_{x \mathop \in S} \norm x_X < \infty$
{{TFAE}}
:$(1): \quad$ $S$ does not contain a basic sequence
:$(2): \quad$ $\map {\cl_w} S$ is compact in $w$ and ${\mathbf 0}_X \not \in \map {\cl_w} S$.

Proof:
=== $(2)$ implies $(1)$ ===
{{AimForCont}} that $S$ contains a basic sequence $\sequence {x_n}_{n \mathop \in \N}$.
Since $\map {\cl_w} S$ is compact in $w$, $\sequence {x_n}_{n \mathop \in \N}$ has a cluster point $x \in \map {\cl_w} S$ in $\struct {X, w}$ by {{Corollary|Characterization of Compactness in terms of Nets}}.
From Weak Cluster Point of Basic Sequence in Banach Space is Zero Vector, it follows that $x = {\mathbf 0}_X$.
Hence ${\mathbf 0}_X \in \map {\cl_w} S$.
This contradicts the assumption that ${\mathbf 0}_X \not \in \map {\cl_w} S$.
Hence $S$ does not contain a basic sequence.
{{qed|lemma}}
Theorem: Subsequence of Basic Sequence in Banach Space is Basic Sequence

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ be a Banach space over $\GF$.
Let $\sequence {x_n}_{n \mathop \in \N}$ be a basic sequence in $\struct {X, \norm {\, \cdot \,}_X}$.
Let $\sequence {x_{n_k} }_{k \mathop \in \N}$ be a subsequence of $\sequence {x_n}_{n \mathop \in \N}$.
Then $\sequence {x_{n_k} }_{k \mathop \in \N}$ is a basic sequence in $\struct {X, \norm {\, \cdot \,}_X}$.

Proof:
By Grunblum's Criterion, there exists $K > 0$ such that for any sequence $\sequence {\alpha_j}_{j \mathop \in \N}$ in $\GF$ such that:
:$\ds \norm {\sum_{j \mathop = 1}^m \alpha_j x_j}_X \le K \norm {\sum_{j \mathop = 1}^n \alpha_j x_j}_X$ for $m \le n$.
In particular, we have:
:$\ds \norm {\sum_{j \mathop = 1}^{n_k} \alpha_j x_j}_X \le K \norm {\sum_{j \mathop = 1}^{n_\ell} \alpha_j x_j}_X$ for $k \le \ell$.
Specify $\alpha_j = 0$ whenever $j \ne n_q$ for all $q \in \N$, and set $\beta_j = \alpha_{n_j}$. 
We then obtain:
:$\ds \norm {\sum_{j \mathop = 1}^k \beta_j x_{n_j} }_X \le K \norm {\sum_{j \mathop = 1}^n \beta_j x_{n_j} }_X$ for $k \le n$
for any sequence $\sequence {\beta_j}_{j \mathop \in \N}$ in $\GF$.
Hence $\sequence {x_{n_k} }_{k \mathop \in \N}$ is a basic sequence by Grunblum's Criterion.
{{qed}}
Theorem: Unique Accumulation Point of Sequence in Weakly Countably Compact Subset of Banach Space is Limit of Sequence

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ be a Banach space over $\GF$.
Let $w$ be the weak topology on $\struct {X, \norm {\, \cdot \,}_X}$.
Let $A \subseteq X$ be countably compact in $\struct {X, w}$.
Let $x \in X$.
Let $\sequence {x_n}_{n \mathop \in \N}$ be a sequence in $A$ such that:
:$x$ is the unique accumulation point of $\sequence {x_n}_{n \mathop \in \N}$ in $\struct {X, w}$. 
Then $\sequence {x_n}_{n \mathop \in \N}$ converges weakly to $x$.

Proof:
Let $\struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }$ be the normed dual space of $\struct {X, \norm {\, \cdot \,}_X}$.
Suppose that $\sequence {x_n}_{n \mathop \in \N}$ does not converge to $x$.
By the definition of weak convergence, there exists $f \in X^\ast$ such that:
:$\map f {x_n} \not \to \map f x$
Hence there exists $\epsilon > 0$ such that for each $k \in \N$ there exists $n_k \ge \max \set {n_1, \ldots, n_{k - 1}, k}$ such that:
:$\cmod {\map f {x_{n_k} } - \map f x} \ge \epsilon$
Hence:
:$\set {k \in \N : \map f {x_{n_k} } \in \map {B_\epsilon} {\map f x} } = \O$
where $\map {B_\epsilon} {\map f x}$ is the open ball in $\C$ centered at $\map f x$ with radius $\epsilon$. 
Hence $\map f x$ is not an accumulation point of $\sequence {x_{n_k} }_{k \mathop \in \N}$ in $\struct {X, w}$.
However, since $A$ is countably compact, $\sequence {x_{n_k} }_{k \mathop \in \N}$ has an accumulation point $z$.
Then $z$ is an accumulation point of $\sequence {x_n}_{n \mathop \in \N}$, contradicting the uniqueness of $x$.
{{qed}}
Theorem: Eberlein-Šmulian Theorem

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ be a Banach space over $\GF$.
Let $w$ be the weak topology on $\struct {X, \norm {\, \cdot \,}_X}$.
Let $A \subseteq X$.
{{TFAE}}
:$(1): \quad$ $\struct {A, w}$ is compact
:$(2): \quad$ $\struct {A, w}$ is sequentially compact in itself
:$(3): \quad$ $\struct {A, w}$ is countably compact.

Proof:
Let $\cl_w$ be the closure taken in $\struct {X, w}$. 
Let $\cl$ be the closure taken in $\struct {X, \norm {\, \cdot \,}_X}$.
Theorem: Countably Compact Metric Space is Bounded

Let $\struct {X, d}$ be a countably compact metric space.
Then $\struct {X, d}$ is bounded.

Proof:
Let $x_0 \in X$. 
Let $\map {B_n} {x_0}$ be the open ball of radius $n$, centered at $x_0$.
Clearly:
:$\ds \bigcup_{n \mathop = 1}^\infty \map {B_n} {x_0} \subseteq X$
For each $x \in X$, we have:
:$x \in \map {B_r} {x_0}$, where $r = \floor {\map d {x, x_0} } + 1$.
Hence, we have:
:$\ds X = \bigcup_{n \mathop = 1}^\infty \map {B_n} {x_0}$
Since $\struct {X, d}$ is countably compact, there exists $n_1, \ldots, n_k \in \N$ such that:
:$\ds X = \bigcup_{j \mathop = 1}^k \map {B_{n_j} } {x_0}$
Taking $R = \max \set {n_1, \ldots, n_k}$, we then have $X = \map {B_R} {x_0}$.
In other words, for each $x \in X$ we have $\map d {x, x_0} < R$.
Hence $\struct {X, d}$ is bounded.
{{qed}}
Category:Countably Compact Spaces
Category:Metric Spaces
lcqae7ziae7cn88w8wx1io7to47ptmb
Theorem: Continuous Image of Countably Compact Space is Countably Compact

Let $\struct {X, \tau_X}$, $\struct {Y, \tau_X}$ be topological spaces.
Let $C \subseteq X$ be countably compact in $\struct {X, \tau_X}$.
Let $f : X \to Y$ be continuous.
Then $f \sqbrk C$ is countably compact.

Proof:
Let $\UU = \set {U_n : n \in \N}$ be a countable open cover of $f \sqbrk C$. 
Since $f$ is continuous, we have $f^{-1} \sqbrk {U_n} \in \tau_X$ for each $n \in \N$.
{{begin-eqn}}
{{eqn	| l = \bigcup_{n \mathop = 1}^\infty f^{-1} \sqbrk {U_n}
		| r = f^{-1} \sqbrk {\bigcup_{n \mathop = 1}^\infty U_n}
		| c = Preimage of Union under Mapping: General Result
}}
{{eqn	| r = f^{-1} \sqbrk {f \sqbrk C}
}}
{{eqn	| o = \supseteq
		| r = C
		| c = Image of Preimage under Mapping
}}
{{end-eqn}}
Hence $\set {f^{-1} \sqbrk {U_n} : n \in \N}$ is an  open cover of $C$.
Since $C$ is countably compact, there exists $N \in \N$ such that:
:$\ds C \subseteq \bigcup_{n \mathop = 1}^N f^{-1} \sqbrk {U_n}$
Hence if $x \in C$, we have $\map f x \in U_n$ for some $1 \le n \le N$. 
Hence we have:
:$\ds f \sqbrk C \subseteq \bigcup_{n \mathop = 1}^N U_n$
So $\set {U_n : 1 \le n \le N}$ is a finite subcover of $\UU$.
Since $\UU$ was arbitrary, we have that $f \sqbrk C$ is countably compact.
{{qed}}
Category:Countably Compact Spaces
dpb25gfjw0ig23qy3o6xpr4q1ez91be
Theorem: Subset of Normed Vector Space providing Bounded Point Evaluations is Norm Bounded

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ be a normed vector space over $\GF$.
Let $\struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }$ be the normed dual of $\struct {X, \norm {\, \cdot \,}_X}$.
Let $S \subseteq X$.
Suppose that:
:$\ds \sup_{x \mathop \in S} \cmod {\map f x} < \infty$
for each $f \in X^\ast$.
Then we have:
:$\ds \sup_{x \mathop \in S} \norm x_X < \infty$
Hence $S$ is bounded.

Proof:
Let $\struct {X^{\ast \ast}, \norm {\, \cdot \,}_{X^{\ast \ast} } }$ be the second normed dual of $\struct {X, \norm {\, \cdot \,}_X}$.
Let $\iota : X \to X^{\ast \ast}$ be the evaluation linear transformation.
We then have:
:$\ds \sup_{x \mathop \in S} \cmod {\map {\iota x} f} < \infty$ for each $f \in X^\ast$.
From Normed Dual Space is Banach Space, $\struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }$ is a Banach space.
From the Banach-Steinhaus Theorem, we have:
:$\ds \sup_{x \mathop \in S} \norm {\iota x}_{X^{\ast \ast} } < \infty$ 
From Evaluation Linear Transformation on Normed Vector Space is Linear Isometry, $\iota$ is an isometry.
Hence:
:$\ds \sup_{x \mathop \in S} \norm x_X < \infty$
{{qed}}
Category:Normed Dual Spaces
3m4gf7e5rfmpirychcazhn6xaz0t5k0
Theorem: Weakly Countably Compact Set in Normed Vector Space is Norm Bounded

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ be a normed vector space over $\GF$.
Let $w$ be the weak topology on $\struct {X, \norm {\, \cdot \,}_X}$.
Let $C \subseteq X$ be $w$-countably compact.
Then:
:$\ds \sup_{x \mathop \in S} \norm x_X < \infty$
Hence $C$ is bounded.

Proof:
Let $X^\ast$ be the normed dual space of $\struct {X, \norm {\, \cdot \,}_X}$.
Let $f \in X^\ast$.
From Continuous Image of Countably Compact Space is Countably Compact, $f \sqbrk C$ is countably compact in $\GF$.
From Countably Compact Metric Space is Bounded, $f \sqbrk C$ is bounded.
Hence for each $f \in X^\ast$ we have:
:$\ds \sup_{x \mathop \in C} \cmod {\map f x} < \infty$
From Subset of Normed Vector Space providing Bounded Point Evaluations is Norm Bounded, we have:
:$\ds \sup_{x \mathop \in C} \norm x_X < \infty$
Hence $C$ is bounded.
{{qed}}
Category:Countably Compact Spaces
Category:Weak Topologies on Topological Vector Spaces
1g2l6k9siny6xgunm2ztled19eo5sh4
Theorem: Accumulation Point of Sequence iff Cluster Point of Net

Let $\struct {X, \tau}$ be a topological space.
Let $\sequence {x_n}_{n \mathop \in \N}$ be a sequence in $X$.
Let $x \in X$.
Then $x$ is an accumulation point of $\sequence {x_n}_{n \mathop \in \N}$ as a sequence {{iff}} $x$ is a cluster point of $\sequence {x_n}_{n \mathop \in \N}$ as a net.

Proof:
=== Necessary Condition ===
Suppose that $x$ is an accumulation point of $\sequence {x_n}_{n \mathop \in \N}$.
Let $U \in \tau$.
Then:
:$\SS = \set {n \in \N : x_n \in U}$ is infinite.
Note that $\set {1, \ldots, K}$ is finite and every subset of a finite set is finite by Subset of Finite Set is Finite.
Hence for each $k \in \N$, there exists $n_k > k$ such that $k \in \SS$, else we would have $\SS \subseteq \set {1, \ldots, K}$.
That is, for each $k \in \N$ there exists $n_k > k$ such that $x_{n_k} \in U$.
Hence $x$ is a cluster point of $\sequence {x_n}_{n \mathop \in \N}$ as a net.
{{qed|lemma}}
Theorem: Interior of Closed Rectangle

Let:
:$\ds \RR = \prod_{i \mathop = 1}^n \closedint {a_i} {b_i}$
be a closed $n$-rectangle.
Then:
:$\ds \RR^\circ = \prod_{i \mathop = 1}^n \openint {a_i} {b_i}$
where $\RR^\circ$ denotes the interior of $\RR$.

Proof:
{{begin-eqn}}
{{eqn | l = \RR^\circ
      | r = \prod_{i \mathop = 1}^n \closedint {a_i} {b_i}^\circ
      | c = Interior of Cartesian Product is Product of Interiors
}}
{{eqn | r = \prod_{i \mathop = 1}^n \openint {a_i} {b_i}
      | c = Interior of Closed Real Interval is Open Real Interval
}}
{{end-eqn}}{{qed}}
Category:Examples of Set Interiors
31aetyl90jd52r7s2ct5fnxjf5wjkna
Theorem: Continuous Mapping Induced by Localic Mapping is Continuous

Let $L_1 = \struct{S_1, \preceq_1}$ and $L_2 = \struct{S_2, \preceq_2}$ be locales.
Let $f : L_1 \to L_2$ be a localic mapping.
Let:
:$\map {\operatorname{Sp}} f : \map {\operatorname{Sp}} {L_1} \to \map {\operatorname{Sp}} {L_2}$ denote the continuous mapping induced by $f$
where:
:$\map {\operatorname{Sp}} {L_1}$ and $\map {\operatorname{Sp}} {L_2}$ denote the spectra as completely prime filters of $L_1$ and $L_2$, respectively
Then:
:$\map {\operatorname{Sp}} f$ is a continuous mapping

Proof:
Let $\loweradjoint f : L_2 \to L_1$ denote the lower adjoint such that $\tuple{f, \loweradjoint f}$ is a Galois connection.
By definition of a localic mapping:
:$\loweradjoint f: L_2 \to L_1$ is a frame homomorphism.
Let:
:$\map {\operatorname{Sp}} {f^*} : \map {\operatorname{Sp}} {L_1} \to \map {\operatorname{Sp}} {L_2}$ denote the continuous mapping induced by frame homomorphism $f^*$
From Continuous Mapping Induced by Frame Homomorphism is Continuous:
:$\map {\operatorname{Sp}} {f^*}$ is a continuous mapping
We have:
{{begin-eqn}}
{{eqn | l = \map {\operatorname{Sp} } f
      | r = \paren{f^*}^\gets \restriction_{\paren{\map {\operatorname{Sp} } {L_2} \times \map {\operatorname{Sp} } {L_1} } } 
      | c = {{Defof|Continuous Mapping Induced by Localic Mapping}}
}}
{{eqn | r = \map {\operatorname{Sp} } {f^*}
      | c = {{Defof|Continuous Mapping Induced by Frame Homomorphism}}
}}
{{end-eqn}}
Hence:
:$\map {\operatorname{Sp}} f$ is a continuous mapping.
{{qed}}
Category:Continuous Maps
Category:Continuous Mappings
ebexgbob9i4nqw896ok4a45x112bf4k
Theorem: Localic Spectrum Functor is Covariant Functor

Let $\mathbf{Loc_*}$ denote the category of locales with localic mappings.
Let $\mathbf{Top}$ denote the category of topological spaces.
Then:
:the localic spectrum functor $\operatorname {Sp} : \mathbf{Loc_*} \to \mathbf{Top}$ is a covariant functor

Proof:
Let $\mathbf{Loc}$ denote the category of locales.
Let $G : \mathbf{Loc_*} \to \mathbf{Loc}$ be defined by:
:for each locale $L$ of $\mathbf{Loc_*} : \map G L = L$
:for each localic mapping $g : L_1 \to L_2$ of $\mathbf{Loc_*} : \map G g = \paren{g^*}^{\operatorname{op}}$
where:
:$g^* : L_2 \to L_1$ denotes the frame homomorphism that is the lower adjoint of the localic mapping $g$
:$\paren{g^*}^{\operatorname{op}}$ denotes the opposite morphism of the frame homomorphism
From Category of Locales with Localic Mappings is Isomorphic to Category of Locales:
:$G$ is an isomorphism of categories
Let $\operatorname {Sp}': \mathbf{Loc} \to \mathbf{Top}$ denote the spectrum functor.
Recall the spectrum functor is defined by:
:
:
From Spectrum Functor is Covariant Functor:
:$\operatorname {Sp}'$ is a covariant functor
Let $\operatorname {Sp}' \mathop \circ G$ denote the composite functor of $\operatorname {Sp}'$ with $G$.
From Composite Functor is Functor:
:$\operatorname {Sp}' \mathop \circ G$ is a covariant functor
Let $L$ be a locale in $\mathbf{Loc_*}$.
We have:
{{begin-eqn}}
{{eqn | l = \map {\operatorname {Sp}' \mathop \circ G} L
      | r = \map {\operatorname {Sp}'} {\map G L}
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = \map {\operatorname {Sp}'} L
      | c = Definition of $G$
}}
{{eqn | r = L
      | c = {{Defof|Spectrum Functor}}
}}
{{eqn | r = \map {\operatorname {Sp} } L
      | c = {{Defof|Localic Spectrum Functor}}
}}
{{end-eqn}}
Let $f : L_1 \to L_2$ be a localic mapping in $\mathbf{Loc_*}$.
We have:
{{begin-eqn}}
{{eqn | l = \map {\operatorname {Sp}' \mathop \circ G} f
      | r = \map {\operatorname {Sp}'} {\map G f}
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = \map {\operatorname {Sp}'} {\paren{f^*}^{\operatorname{op} } }
      | c = Definition of $G$
}}
{{eqn | r = \paren{f^*}^{\gets} \restriction_{\paren{\map {\operatorname{Sp} } {L_1} \times \map {\operatorname{Sp} } {L_2} } } 
      | c = {{Defof|Spectrum Functor}}
}}
{{eqn | r = \map {\operatorname {Sp} } f
      | c = {{Defof|Localic Spectrum Functor}}
}}
{{end-eqn}}
It follows that:
:$\operatorname {Sp} = \operatorname {Sp}' \mathop \circ G$
Hence $\operatorname {Sp}$ is a covariant functor.
{{qed}}
Theorem: Point in Closure of Sequence in Metric Space is Term of Sequence or Subsequential Limit

Let $\struct {X, d}$ be a metric space.
Let $\sequence {x_n}_{n \mathop \in \N}$ be a sequence in $X$.
Let $\cl$ be the closure taken in $X$.
Let $x \in \map \cl {\sequence {x_n}_{n \mathop \in \N} }$.
Then either there exists $n \in \N$ with $x = x_n$ or there exists a subsequence $\sequence {x_{n_k} }_{k \mathop \in \N}$ converging to $x$.

Proof:
Suppose that $x_n \ne x$ for all $n \in \N$. 
From Point in Closure of Subset of Metric Space iff Limit of Sequence, there exists a sequence $\sequence {y_n}_{n \mathop \in \N}$ in $\map \cl {\sequence {x_n}_{n \mathop \in \N} }$ such that $y_n \to x$ in $\struct {X, d}$.
Write $y_n = x_{\map \phi n}$. 
Since $x_n \ne x$ for all $n \in \N$, it cannot be the case that $\sequence {y_n}_{n \mathop \in \N}$ is eventually constant.
Since $\map d {y_n, x} > 0$ for each $n \in \N$, it must also be the case that $\sequence {\map \phi n}_{n \mathop \in \N}$ is unbounded.
Pick $N_1 = \map \phi 1$.
For each $k \ge 2$, there exists $N_k \in \N$ such that $N_k > \max \set {N_1, \ldots, N_{k - 1} }$ and $\map \phi {N_k} > \max \set {\map \phi {N_1}, \ldots, \map \phi {N_{k - 1} }}$. 
Set $n_k = \map \phi {N_k}$ for each $k \in \N$.
Then $\sequence {x_{n_k} }_{k \mathop \in \N}$ is a subsequence of $\sequence {x_n}_{n \mathop \in \N}$.
Since $\sequence {x_{n_k} }_{k \mathop \in \N}$ is also a subsequence of $\sequence {y_n}_{n \mathop \in \N}$. 
From Limit of Subsequence equals Limit of Sequence, $\sequence {x_{n_k} }_{k \mathop \in \N}$ converges to $x$.
{{qed}}
Category:Metric Spaces
13cs0qw6xrfe7ly00lffq2zniwtt198