avewright/proofwiki-math huggingface dataset:
Theorem: Equivalence of Definitions of Limit Point of Set/Definition from Open Neighborhood iff Definition from Relative Complement

Let $T = \struct {S, \tau}$ be a topological space.
Let $A \subseteq S$.
{{TFAE|def = Limit Point of Set|view = limit point}}
=== Definition from Open Neighborhood===
{{:Definition:Limit Point of Set/Definition from Open Neighborhood}}
=== Definition from Relative Complement===
{{:Definition:Limit Point of Set/Definition from Relative Complement}}

Proof:
The following equivalence holds:
There exists an open neighborhood $U$ of $x$ such that $A \cap \paren {U \setminus \set x} = \O$
{{begin-eqn}}
{{eqn | l = \O
      | r = A \cap \paren {U \setminus \set x}
}}
{{eqn | ll = \leadstoandfrom
      | l  = \O
      | r  = \paren {U \cap A} \setminus \set x
      | cc = Intersection with Set Difference is Set Difference with Intersection
}}
{{eqn | ll = \leadstoandfrom
      | l  = \O
      | r  = \paren {A \cap U} \setminus \set x
      | cc = Intersection is Commutative
}}
{{eqn | ll = \leadstoandfrom
      | l  = \O
      | r  = U \cap \paren {A \setminus \set x}
      | cc = Intersection with Set Difference is Set Difference with Intersection
}}
{{eqn | ll = \leadstoandfrom
      | l  = \O
      | r  = U \cap \map \complement {\map \complement {A \setminus \set x} }
      | cc = Complement of Complement
}}
{{eqn | ll = \leadstoandfrom
      | l  = U
      | o  = \subseteq
      | r  = \map \complement {A \setminus \set x}
      | cc = Intersection with Complement is Empty iff Subset
}}
{{eqn | ll = \leadstoandfrom
      | l  = U
      | o  = \subseteq
      | r  = \map \complement {A \cap \map \complement {\set x} }
      | cc = Set Difference as Intersection with Complement
}}
{{eqn | ll = \leadstoandfrom
      | l  = U
      | o  = \subseteq
      | r  = \map \complement A \cup \map \complement {\map \complement {\set x} }
      | cc = De Morgan's Laws (Set Theory)/Set Complement
}}
{{eqn | ll = \leadstoandfrom
      | l  = U
      | o  = \subseteq
      | r  = \map \complement A \cup \set x
      | cc = Complement of Complement
}}
{{end-eqn}}
By {{Defof|Neighborhood of Point}}, $\map \complement A \cup \set x$ is a neighborhood of $x$
The result follows from the Rule of Transposition.
{{qed}}
Theorem: Equivalence of Definitions of Limit Point in Metric Space

Let $M = \struct {S, d}$ be a metric space.
Let $\tau$ be the topology induced by the metric $d$.
Let $A \subseteq S$ be a subset of $S$.
Let $\alpha \in S$. 
{{TFAE|def = Limit Point/Metric Space|view = limit point in metric space}}
=== Definition 1 ===
{{:Definition:Limit Point/Metric Space/Definition 1}}
=== Definition 2 ===
{{:Definition:Limit Point/Metric Space/Definition 2}}
=== Definition 3 ===
{{:Definition:Limit Point/Metric Space/Definition 3}}

Proof:
=== $(1) \implies (2)$ ===
Let:
:$\forall \epsilon \in \R_{>0}: \paren {\map {B_\epsilon} \alpha \setminus \set \alpha} \cap A \ne \O$
{{:Equivalence of Definitions of Limit Point in Metric Space/Definition 1 implies Definition 2}}{{qed|lemma}}
Theorem: Equivalence of Definitions of Limit Point in Metric Space/Definition 1 implies Definition 2

Let $M = \struct {S, d}$ be a metric space.
Let $\tau$ be the topology induced by the metric $d$.
Let $A \subseteq S$ be a subset of $S$.
Let $\alpha \in S$. 
Let:
:$\forall \epsilon \in \R_{>0}: \paren {\map {B_\epsilon} \alpha \setminus \set \alpha} \cap A \ne \O$
Then:
:there is a sequence $\sequence{\alpha_n}$ in $A$ such that $\alpha$ is a limit of the sequence $\sequence{\alpha_n}$, considered as sequence in $S$.

Proof:
A sequence $\sequence {\alpha_n}$ is constructed using finite recursion.
Let $\alpha_0$ be some arbitrary point in $A \cap \paren{\map {B_1} \alpha \setminus \set \alpha}$.
$\alpha_{n + 1}$ is some arbitrary point in $A \cap \paren{\map {B_{\frac {\map d {\alpha, \alpha_n} } 2} } \alpha \setminus \set \alpha}$ where $\map {B_{\frac {\map d {\alpha, \alpha_n} } 2} } \alpha$ denotes the open $\dfrac {\map d {\alpha, \alpha_n} } 2$-ball of $\alpha$.
We can be assured that such a point exists {{hypothesis}}.
Then:
:$\map d {\alpha_n, \alpha} < 2^{-n} \map d {\alpha_0, \alpha}$
Since $\map d {\alpha_0, \alpha}$ is fixed:
:$\map d {\alpha_n, \alpha} < 2^{-n} \map d {\alpha_0, \alpha} < r$
for some $n$ because the natural numbers are Archimedean.
Therefore $\alpha$ is the limit of the sequence $\sequence {\alpha_n}$ by definition.
Theorem: Equivalence of Definitions of Extreme Point of Convex Set

{{finish|The definitions have changed}}
{{TFAE|def = Extreme Point of Convex Set}}
Let $X$ be a vector space over $\R$. 
Let $K$ be a convex subset of $X$. 
=== Definition 1 ===
{{:Definition:Extreme Point of Convex Set/Definition 1}}
=== Definition 2 ===
{{:Definition:Extreme Point of Convex Set/Definition 2}}

Proof:
=== Definition 1 implies Definition 2 ===
Suppose that: 
:whenever $a = t x + \paren {1 - t} y$ for $t \in \openint 0 1$, we have $x = y = a$.
Then, if $x, y \in K \setminus \set a$ and $t \in \openint 0 1$, we have: 
:$t x + \paren {1 - t} y \ne a$ 
If $t = 0$, then we have: 
:$t x + \paren {1 - t} y = y \ne a$
and if $t = 1$ we have: 
:$t x + \paren {1 - t} y = x \ne a$ 
So if $x, y \in K \setminus \set a$ and $t \in \closedint 0 1$ we have:
:$t x + \paren {1 - t} y \ne a$ 
Since $K$ is convex, we have: 
:$t x + \paren {1 - t} y \in K$
so we have: 
:$t x + \paren {1 - t} y \in K \setminus \set a$
so:
:$K \setminus \set a$ is convex.
{{qed|lemma}}
Theorem: Axioms of Hilbert Proof System Instance 1 for Predicate Logic are Tautologies

Let $\mathscr H$ be Instance 1 of a Hilbert proof system for predicate logic.
Then the axioms of $\mathscr H$ are tautologies.

Proof:
{{improve|For each axiom this should link to a theorem page instead, but I had difficulties coming up with names. Maybe subpages?}}
=== Axiom 1 ===
This is precisely the statement of Propositional Tautology is Tautology in Predicate Logic.
{{qed|lemma}}
{{proofread|below}}
{{improve|The theorem cited below is actually Universal Generalisation for semantics of PredLog}}
By Well-Formed Formula is Tautology iff Universal Closure is Tautology, we prove the results for axioms 2 through 11 for the WFFs instead of their universal closures.
Let $\sigma$ be an assignment in a structure $\AA$.
Let $\map { \operatorname{val}_\AA } {\cdot} \sqbrk \sigma$ be the value mapping for $\sigma$ in $\AA$.
Theorem: Equivalence of Definitions of Limit Point in Metric Space/Definition 2 implies Definition 3

Let $M = \struct {S, d}$ be a metric space.
Let $\tau$ be the topology induced by the metric $d$.
Let $A \subseteq S$ be a subset of $S$.
Let $\alpha \in S$. 
Let there exist a sequence $\sequence{\alpha_n}$ in $A \setminus \set \alpha$ such that $\sequence{\alpha_n}$ converges to $\alpha$ in $S$.
Then:
:$\alpha$ is a limit point in the topological space $\struct{S, \tau}$.

Proof:
Let $U \in \tau$ be an arbitrary open set:
:$\alpha \in U$
By {{Defof|Topology Induced by Metric}}:
:$\exists \epsilon \in \R_{>0} : \map {B_\epsilon} \alpha \subseteq U$
By {{Defof|Convergent Sequence (Metric Space)}}:
:$\exists N \in \N : \forall n \ge N : d(\alpha, \alpha_n) < \epsilon$
By {{Defof|Open Ball}}:
:$\alpha_N \in \map {B_\epsilon} \alpha$
By hypothesis:
:$\alpha_N \in A \setminus \set \alpha$
We have:
{{begin-eqn}}
{{eqn | l = \alpha_N \in \paren{A \setminus \set \alpha} \cap \map {B_\epsilon} \alpha
      | r = \paren{A \cap \map {B_\epsilon} \alpha} \setminus \set \alpha
      | c = Intersection with Set Difference is Set Difference with Intersection
}}
{{eqn | o = \subseteq
      | r = \paren{A \cap U} \setminus \set \alpha
      | c = Set Intersection Preserves Subsets and Set Difference over Subset
}}
{{eqn | r = A \cap \paren{U \setminus \set \alpha}
      | c = Intersection with Set Difference is Set Difference with Intersection
}}
{{end-eqn}}
Hence:
:$A \cap \paren{U \setminus \set \alpha} \ne \O$
Since $U$ was arbitrary, it follows that $\alpha$ is a limit point in the topological space $\struct{S, \tau}$ by definition.
Theorem: Equivalence of Definitions of Limit Point in Metric Space/Definition 3 implies Definition 1

Let $M = \struct {S, d}$ be a metric space.
Let $\tau$ be the topology induced by the metric $d$.
Let $A \subseteq S$ be a subset of $S$.
Let $\alpha \in S$. 
Let $\alpha$ be a limit point in the topological space $\struct{S, \tau}$.
Then:
:$\forall \epsilon \in \R_{>0}: \paren {\map {B_\epsilon} \alpha \setminus \set \alpha} \cap A \ne \O$

Proof:
From Open Ball is Open Set:
:$\forall \epsilon \in \R_{>0}: \map {B_\epsilon} \alpha$ is open set in $M$
By {{Defof|Topology Induced by Metric}}:
:$\forall \epsilon \in \R_{>0}: \map {B_\epsilon} \alpha$ is open set in $\struct{S,\tau}$
By {{Defof|Limit Point of Set}}:
:$\forall \epsilon \in \R_{>0}: \paren {\map {B_\epsilon} \alpha \setminus \set \alpha} \cap A \ne \O$
Theorem: Union minus Symmetric Difference equals Intersection

:$\paren {A \cup B} \setminus \paren {A \symdif B} = A \cap B$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {A \cup B} \setminus \paren {A \symdif B}
      | r = \paren {A \cup B} \setminus \paren {\paren {A \cup B} \setminus \paren {A \cap B} }
      | c = {{Defof|Symmetric Difference|index = 2}}
}}
{{eqn | r = \paren {A \cup B} \cap \paren {A \cap B}
      | c = Set Difference with Set Difference
}}
{{eqn | r = A \cap B
      | c = Intersection of Union with Intersection
}}
{{end-eqn}}
{{qed}}
Category:Set Union
Category:Set Intersection
Category:Symmetric Difference
9trfs5bh12677ko5lgr7w4a1wqporkk
Theorem: Locally Convex Space is Hausdorff iff induces Hausdorff Topology

Let $\struct {X, \mathcal P}$ be a locally convex space.
Let $\tau$ be the standard topology on $\struct {X, \mathcal P}$.
Then $\struct {X, \mathcal P}$ is Hausdorff {{iff}} $\struct {X, \tau}$ is a Hausdorff topological space.

Proof:
=== Sufficient Condition ===
Suppose that $\struct {X, \tau}$ is a Hausdorff space.
Let $x \in X$ have $x \ne {\mathbf 0}_X$.
If there exists no such $x$, then we have the claim by vacuous truth.
Otherwise, since $\struct {X, \tau}$ is Hausdorff, there exists $U, V \in \tau$ with $x \in U$ and ${\mathbf 0}_X \in V$ and $U \cap V = \O$. 
Then $x \not \in V$ and ${\mathbf 0}_X \not \in V$.
From Open Sets in Standard Topology of Locally Convex Space, there exists $\epsilon > 0$ and seminorms $p_1, p_2, \ldots, p_n$ such that: 
:$\set {z \in X : \map {p_k} z < \epsilon, \text { for all } k \in \set {1, 2, \ldots, n} } \subseteq V$
Then we have, since $x \not \in V$:
:$x \not \in \set {z \in X : \map {p_k} z < \epsilon, \text { for all } k \in \set {1, 2, \ldots, n} }$
Then there exists $k \in \set {1, 2, \ldots, n}$ such that: 
:$\map {p_k} x \ge \epsilon > 0$ 
In particular: 
:$\map {p_k} x \ne 0$
with $p_k \in \mathcal P$.
So $\struct {X, \mathcal P}$ is Hausdorff.
{{qed|lemma}}
Theorem: Seminorm Maps Zero Vector to Zero

Let $\struct {K, +, \circ}$ be a division ring with norm $\norm {\,\cdot\,}_K$.
Let $X$ be a vector space over $\struct {K, \norm {\,\cdot\,}_K}$.
Let $\mathbf 0_X$ be the zero vector of $X$.
Let $p$ be a seminorm on $X$.
Then $\map p {\mathbf 0_X} = 0$.

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \map p {\mathbf 0_X}
      | r = \map p {0 \circ \mathbf 0_X}
      | c = Zero Vector Scaled is Zero Vector
}}
{{eqn | r = \norm 0_K \map p {\mathbf 0_X}
      | c = $(\text N 2)$ in {{Defof|Seminorm}}
}}
{{eqn | r = 0 \; \map p {\mathbf 0_X}
      | c = $(\text N 1)$ in {{Defof|Norm on Division Ring}}
}}
{{eqn | r = 0
}}
{{end-eqn}}
{{qed}}
Category:Seminorms
Category:Zero Vectors
njfzayzl57w7v4734xr3lpj6556f61d
Theorem: Principle of Superinduction

Let $A$ be a class.
Let $g: A \to A$ be a mapping on $A$.
Let $A$ be minimally superinductive under $g$.
Let $P: A \to \set {\T, \F}$ be a propositional function on $A$.
Suppose that:
{{begin-axiom}}
{{axiom | n = 1
        | m = \map P \O = \T
}}
{{axiom | n = 2
        | q = \forall x \in A
        | m = \map P x = \T \implies \map P {\map g x} = \T
}}
{{axiom | n = 3
        | q = \forall C: \forall x \in C
        | m = \map P x = \T \implies \map P {\bigcup C} = \T
        | rc= where $C$ is a chain of elements of $A$
}}
{{end-axiom}}
Then:
:$\forall x \in A: \map P x = \T$

Proof:
We are given that $A$ is a minimally superinductive class under $g$.
That is, $A$ is a superinductive class under $g$ with the extra property that for $A$ has no proper class which is also superinductive under $g$.
Let $P$ be a propositional function on $A$ which has the properties specified:
{{begin-axiom}}
{{axiom | n = 1
        | m = \map P \O = \T
}}
{{axiom | n = 2
        | q = \forall x \in A
        | m = \map P x = \T \implies \map P {\map g x} = \T
}}
{{axiom | n = 3
        | q = \forall C: \forall x \in C
        | m = \map P x = \T \implies \map P {\bigcup C} = \T
        | rc= where $C$ is a chain of elements of $A$
}}
{{end-axiom}}
Then by definition, the class $S$ of all elements of $A$ such that $\map P x = \T$ is a superinductive class under $g$.
But because $A$ is minimally superinductive under $g$, $S$ contains all elements of $A$.
That is:
:$\forall x \in A: \map P x = \T$
as we were to show.
{{Qed}}
Theorem: Double Superinduction Principle

Let $M$ be a class.
Let $g: M \to M$ be a mapping on $M$.
Let $M$ be a minimally superinductive class under $g$.
Let $\RR$ be a relation on $M$ which satisfies:
{{begin-axiom}}
{{axiom | n = \text D_1
        | q = \forall x \in M
        | m = \map \RR {x, \O}
}}
{{axiom | n = \text D_2
        | q = \forall x, y \in M
        | m = \map \RR {x, y} \land \map \RR {y, x} \implies \map \RR {x, \map g y}
}}
{{axiom | n = \text D_3
        | q = \forall x \in M: \forall C: \forall y \in C
        | m = \map \RR {x, y} \implies \map \RR {x, \bigcup C}
        | rc= where $C$ is a chain of elements of $M$
}}
{{end-axiom}}
Then $\map \RR {x, y}$ holds for all $x, y \in M$.

Proof:
The proof proceeds by Proof by Superinduction.
Let an element $x$ of $M$ be defined as:
:'''left normal''' with respect to $\RR$ {{iff}} $\map \RR {x, y}$ for all $y \in M$
:'''right normal''' with respect to $\RR$ {{iff}} $\map \RR {y, x}$ for all $y \in M$.
Let the hypothesis be assumed.
First we demonstrate a lemma:
Theorem: Pasting Lemma/Union of Open Sets

Let $T = \struct {X, \tau}$ and $S = \struct {Y, \sigma}$ be topological spaces.
Let $I$ be an indexing set.
Let $\family {C_i}_{i \mathop \in I}$ be a family of open sets of $T$.
Let $f: X \to Y$ be a mapping such that the restriction $f \restriction_{C_i}$ is continuous for all $i \in I$.
Then $f$ is continuous on $C = \ds \bigcup_{i \mathop \in I} C_i$, that is, $f \restriction_C$ is continuous.

Proof:
Let $V$ be an open set of $S$.
By assumption, we have that, for all $i \in I$, $U_i = \paren {f \restriction_{C_i} }^{-1} \sqbrk V$ is also open in $T$.
By {{Defof|Restriction of Mapping}}, we have that $U_i = C_i \cap f^{-1} \sqbrk V$.
Therefore, we can compute:
{{begin-eqn}}
{{eqn | l = \paren {f \restriction_C}^{-1} \sqbrk V
      | r = C \cap f^{-1} \sqbrk V
      | c = {{Defof|Restriction of Mapping}}
}}
{{eqn | r = \paren {\bigcup_{i \mathop \in I} C_i} \cap f^{-1} \sqbrk V
      | c = Definition of $C$
}}
{{eqn | r = \bigcup_{i \mathop \in I} \paren {C_i \cap f^{-1} \sqbrk V}
      | c = Intersection Distributes over Union
}}
{{eqn | r = \bigcup_{i \mathop \in I} U_i
      | c = Definition of $U_i$
}}
{{end-eqn}}
That is, $U = \paren {f \restriction_C}^{-1} \sqbrk V$ is a union of open sets.
Therefore, $U$ is itself open by definition of topology.
It follows that $f \restriction_C$ is also continuous by definition.
{{qed}}
Theorem: Pasting Lemma/Finite Union of Closed Sets

Let $T = \struct {X, \tau}$ and $S = \struct {Y, \sigma}$ be topological spaces.
Let $I$ be a finite indexing set.
Let $\family {C_i}_{i \mathop \in I}$ be a finite family of closed sets of $T$.
Let $f: X \to Y$ be a mapping such that the restriction $f \restriction_{C_i}$ is continuous for all $i \in I$.
Then $f$ is continuous on $C = \ds \bigcup_{i \mathop \in I} C_i$, that is, $f \restriction_C$ is continuous.

Proof:
Let $V \subset S$ be a closed set.
By Continuity Defined from Closed Sets, we have that $U_i = \paren {f \restriction_{C_i} }^{-1} \sqbrk V$ is also closed.
From the definition of a restriction, we have that $U_i = C_i \cap f^{-1} \sqbrk V$.
Therefore, we can compute:
{{begin-eqn}}
{{eqn | l = \paren {f \restriction_{C_i} }^{-1} \sqbrk V
      | r = C \cap f^{-1} \sqbrk V
      | c = {{Defof|Restriction of Mapping}}
}}
{{eqn | r = \paren {\bigcup_{i \mathop \in I} C_i} \cap f^{-1} \sqbrk V
      | c = Definition of $C$
}}
{{eqn | r = \bigcup_{i \mathop \in I} \paren {C_i \cap f^{-1} \sqbrk V}
      | c = Intersection Distributes over Union
}}
{{eqn | r = \bigcup_{i \mathop \in I} U_i
      | c = Definition of $U_i$
}}
{{end-eqn}}
That is, $U = \paren {f \restriction_{C_i} }^{-1} \sqbrk V$ is the union of finitely many closed sets.
Therefore, $U$ is itself closed by definition of a topology.
It follows by Continuity Defined from Closed Sets that $f \restriction_C$ is also continuous.
{{qed}}
Theorem: Pasting Lemma/Counterexample of Infinite Union of Closed Sets

Let $T = \struct {X, \tau}$ and $S = \struct {Y, \sigma}$ be topological spaces.
Let $I$ be an infinite indexing set.
For all $i \in I$, let $C_i$ be closed in $T$.
Let $f: X \to Y$ be a mapping such that the restriction $f \restriction_{C_i}$ is continuous for all $i$.
Then it does not necessarily hold that $f$ is continuous on $C = \ds \bigcup_{i \mathop \in I}C_i$.
That is, it is not necessarily the case that $f \restriction_C$ is continuous.

Proof:
Let $f : \closedint {-1} 1 \to \R$ be the function on the closed interval $\closedint {-1} 1$ defined by:
:<nowiki>$\map f x  = \begin{cases}
1 & : x \ge 0 \\
-1 & : x < 0 
\end{cases}$</nowiki>
The function $f$ is discontinuous at $0$.
The function $f$ restricted to the closed intervals:
:$\closedint {-1} {-\dfrac 1 2}, \closedint {-1} {-\dfrac 1 3}, \ldots, \closedint {-1} {-\dfrac 1 n}, \ldots, \closedint 0 1$
are constant functions.
From Constant Function is Continuous, the function $f$ restricted to the closed intervals:
:$\closedint {-1} {-\dfrac 1 2}, \closedint {-1} {-\dfrac 1 3}, \ldots, \closedint {-1} {-\dfrac 1 n}, \ldots, \closedint 0 1$
are continuous.
We have:
:$\closedint {-1} 1 = \paren {\ds \bigcup_{n \mathop \in \N_{>1} } \closedint {-1} {-\dfrac 1 n} } \cup \closedint 0 1$
The result follows.
Theorem: Soundness Theorem for Hilbert Proof System for Predicate Logic

Let $\mathscr H$ be instance 1 of a Hilbert proof system for predicate logic.
Let $\mathrm{PL}$ be the formal semantics of structures for predicate logic.
Then $\mathscr H$ is a strongly sound proof system for $\mathrm{PL}$:
:Every $\mathscr H$-provable consequence is a $\mathrm{PL}$-semantic consequence.

Proof:
By Modus Ponendo Ponens for Semantic Consequence in Predicate Logic, the sole rule of inference of $\mathscr H$ preserves $\mathrm{PL}$-semantic consequence.
By definition a $\mathscr H$-provable consequence $\FF \vdash_{\mathscr H} \mathbf A$ means that $\mathbf A$ is a theorem of $\map {\mathscr H} \FF$.
It is to be shown that the semantic consequence $\FF \models_{\mathrm{PL}} \mathbf A$ holds.
Suppose that $\AA$ is a structure for $\mathrm{PL}$ such that $\AA \models_{\mathrm{PL}} \FF$.
:By Axioms of Hilbert Proof System Instance 1 for Predicate Logic are Tautologies, the axioms of $\mathscr H$ are tautologies
:By hypothesis, the extra axioms $\FF$ of $\map {\mathscr H} \FF$ are also valid in $\AA$
Therefore all axioms of $\map {\mathscr H} \FF$ are valid in $\AA$.
Since $\AA$ was arbitrary, it follows that all axioms of $\map {\mathscr H} \FF$ are semantic consequences of $\FF$.
By Modus Ponendo Ponens for Semantic Consequence in Predicate Logic, the sole rule of inference of $\mathscr H$ preserves $\mathrm{PL}$-semantic consequence.
Therefore every theorem of $\map {\mathscr H} \FF$ is a semantic consequences of $\FF$.
Thus, since $\mathbf A$ is a $\map {\mathscr H} \FF$-theorem:
:$\FF \models_{\mathrm{PL}} \mathbf A$
as desired.
{{qed}}
Theorem: Metric on Shift of Finite Type is Metric

Let $\struct {X _\mathbf A, \sigma_\mathbf A}$ be a shift of finite type.
Let $\theta \in \openint 0 1$.
Then the metric $d_\theta$ is indeed a metric on $X_\mathbf A$.
That is, $\struct {X _\mathbf A, d _\theta} $ is a metric space.

Proof:
=== M1 ===
Let $x\in X _\mathbf A$
Obviously, $x_i = x_i$ for all $i \in \openint {-\infty} \infty$.
Therefore:
:$\map {d _\theta} {x,x} = \theta ^\infty = 0$.
{{qed|lemma}}
Theorem: G-Tower is Nest

Let $M$ be a class.
Let $g: M \to M$ be a progressing mapping on $M$.
Let $M$ be a $g$-tower.
Then $M$ is a nest.

Proof:
We need to show that:
:$\forall x, y \in M: x \subseteq y$ or $y \subseteq x$
First some lemmata:
Theorem: Sandwich Principle for G-Towers

Let $M$ be a class.
Let $g: M \to M$ be a progressing mapping on $M$.
Let $M$ be a $g$-tower.
Let $x, y \in M$ be arbitrary.
Then it cannot be the case that:
:$x \subsetneqq y \subsetneqq \map g x$

Proof:
From Lemma $2$ of $g$-Tower is Nest we have that:
:$\forall x, y \in M: \map g x \subseteq y \lor y \subseteq x$
From the Sandwich Principle:
:$\forall x, y \in M: x \subseteq y \subseteq \map g x \implies x = y \lor y = \map g x$
That is, there is no element $y$ of $M$ such that:
:$x \subsetneqq y \subsetneqq \map g x$
{{qed}}
Theorem: Sandwich Principle for G-Towers/Corollary 1

Let $M$ be a class.
Let $g: M \to M$ be a progressing mapping on $M$.
Let $M$ be a $g$-tower.
Let $x, y \in M$ be arbitrary.
Then:
:$x \subsetneqq y \implies \map g x \subseteq y$

Proof:
From {{Lemma|G-Tower is Nest|2|disp = $g$-Tower is Nest|proof = yes}}:
:$\forall x, y \in M: \map g x \subseteq y \lor y \subseteq x$
From {{Corollary|Sandwich Principle|1}}:
:$\forall x, y \in M: x \subseteq y \subseteq \map g x \implies x = y \lor y = \map g x$
That is, if:
:$x \subsetneqq y$
then:
:$\map g x \subseteq y$
{{qed}}
Theorem: Sandwich Principle for G-Towers/Corollary 2

Let $M$ be a class.
Let $g: M \to M$ be a progressing mapping on $M$.
Let $M$ be a $g$-tower.
Let $x, y \in M$ be arbitrary such that $x \subseteq y$.
Then:
:$\map g x \subseteq \map g y$

Proof:
From {{Lemma|G-Tower is Nest|2|disp = $g$-Tower is Nest|proof = yes}}:
:$\forall x, y \in M: \map g x \subseteq y \lor y \subseteq x$
From {{Corollary|Sandwich Principle|2}}:
:$\forall x, y \in M: x \subseteq y\implies \map g x \subseteq \map g y$
{{qed}}
Theorem: Union of Mappings which Agree is Mapping/Family of Mappings

Let $Y$ be a set.
Let $\family {A_i}_{i \mathop \in I}$ be a family of sets indexed by $I$.
Let $\family {f_i: A_i \to Y}$ be a family of mappings indexed by $I$.
Let $X = \ds \bigcup_{i \mathop \in I} A_i$.
Let $f = \ds \bigcup_{i \mathop \in I} f_i : X \to Y$ where $\ds \bigcup_{i \mathop \in I} f_i$ is the union of relations.
Let for all $i, j \in I$, $f_i$ and $f_j$ agree on $A_i \cap A_j$.
Then:
:$f : X \to Y$ is a mapping

Proof:
By Union of Relations is Relation, $f = \ds \bigcup_{i \mathop \in I} f_i$ is a relation whose domain is $X = \ds \bigcup_{i \mathop \in I} A_i$.
Let $\tuple {x, y_1}, \tuple {x, y_2} \in f$.
Then there exists $i, j \in I$ such that:
:$\tuple {x, y_1} \in f_i$ and $\tuple {x, y_2} \in f_j$
Theorem: Pasting Lemma/Continuous Mappings on Open Sets

Let $T = \struct {X, \tau}$ and $S = \struct {Y, \sigma}$ be topological spaces.
Let $I$ be an indexing set.
Let $\family {C_i}_{i \mathop \in I}$ be a family of open sets of $T$.
Let $\family {f_i : C_i \to Y}_{i \mathop \in I}$ be a family of continuous mappings.
Let $C = \ds \bigcup_{i \mathop \in I} C_i$.
Let $f = \ds \bigcup_{i \mathop \in I} f_i : C \to Y$ where $\ds \bigcup_{i \mathop \in I} f_i$ is the union of relations.
Let for all $i, j \in I$, $f_i$ and $f_j$ agree on $C_i \cap C_j$.
Then $f$ is a continuous mapping on $C = \ds \bigcup_{i \mathop \in I} C_i$.

Proof:
From Union of Family of Mappings which Agree is Mapping:
:$f$ is a mapping from $C$ to $Y$.
From Restriction of Union of Mappings which Agree Equals Mapping:
:$\forall i \in I : f \restriction_{C_i} = f_i$
Hence:
:$\forall i \in I : f \restriction_{C_i}$ is continuous
From Pasting Lemma for Union of Open Sets
:$f$ is continuous.
{{qed}}