nyuuzyou/wikis huggingface dataset:
T3 Space with Sigma-Locally Finite Basis is T4 Space/Lemma 1

== Theorem ==
Let $T = \struct {S, \tau}$ be a $T_3$ topological space.
Let $\BB$ be a $\sigma$-locally finite basis.
Let $F$ be a closed subset of $T$.
Let $X \subseteq S$ be disjoint from $F$.
Then there exists a countable open cover $\WW = \set{W_n : n \in \N}$ of $X$:
:$\forall n \in \N : W_n^- \cap F = \O$
== Proof ==
Let $\UU = \set {U \in \BB : U^- \cap F = \O}$.
=== Lemma 2 ===
From Lemma 2:
:$\forall x \in X : \exists U_x \in \BB : x \in U_x : U_x^- \cap B = \O$
Hence:
:$\forall x \in X : \exists U_x \in \UU$
By definition of open cover:
:$\UU$ is an open cover of $X$
By definition of $\sigma$-locally finite:
:$\BB = \ds \bigcup_{n \in \N} \BB_n$
where $\BB_n$ is a locally finite set of subsets.
For each $n \in \N$, let:
:$\UU_n = \UU \cap \BB_n$
From Subset of Locally Finite Set of Subsets is Locally Finite:
:$\UU_n$ is locally finite
For each $n \in \N$, let:
:$W_n = \ds \bigcup \set{W : W \in \UU_n}$
From :
:$W_n \in \tau$
From Union of Closures of Elements of Locally Finite Set is Closed:
:$W_n^- = \ds \bigcup \set{W^- : W \in \UU_n}$
We have:
Let $x \in X$.
From Lemma 2:
:$\exists U_x \in \BB : x \in U_x : U_x^- \cap F = \O$
By definition of $\UU$:
:$U_x \in \UU'$
As $\BB = \ds \bigcup_{n \in \N} \BB_n$:
:$\exists n \in \N : U_x \in \BB_n : x \in U_x : U_x^- \cap F = \O$
Hence:
:$U_x \in \UU_n$
From Set is Subset of Union:
:$U_x \subseteq \ds \bigcup \UU_n = W_n$
Hence:
:$x \in W_n$
By definition, $\WW = \set{W_n : n \in \N}$ is a countable open cover of $X$.
Category:T3 Space with Sigma-Locally Finite Basis is T4 Space
T3 Space with Sigma-Locally Finite Basis is T4 Space/Lemma 2

== Theorem ==
Let $T = \struct {S, \tau}$ be a $T_3$ topological space.
Let $\BB$ be a $\sigma$-locally finite basis.
Let $F$ be a closed subset of $T$.
Let $x \in S \setminus F$.
Then:
:$\exists U \in \BB : x \in U : U^- \cap F = \O$
== Proof ==
From Characterization of T3 Space:
:$\exists W \in \tau: x \in W : W^- \cap F = \O$
By definition of basis:
:$\exists U \in \BB : x \in U \subseteq W$
From Topological Closure of Subset is Subset of Topological Closure:
:$U^- \subseteq W^-$
From Set Intersection Preserves Subsets:
:$U^- \cap F = \O$
Category:T3 Space with Sigma-Locally Finite Basis is T4 Space
T3 Space with Sigma-Locally Finite Basis is T4 Space/Proof 1

== Theorem ==
== Proof ==
Let $A$ and $B$ be disjoint closed subsets of $T$.
=== Lemma 1 ===
From Lemma 1, there exists a countable open cover $\UU = \set{U_n : n \in \N}$ of $A$:
:$\forall n \in \N : U_n^- \cap B = \O$ 
and
there exists a countable open cover $\VV = \set{V_n : n \in \N}$ of $B$:
:$\forall n \in \N : V_n^- \cap A = \O$ 
From Countable Open Covers Condition for Separated Sets:
:$A$ and $B$ can be separated in $T$ 
By definition of separated:
:there exists $U, V \in \tau$ such that $A \subseteq U, B \subseteq V$ and $U \cap V = \O$
Since $A$ and $B$ were arbitrary disjoint closed subsets of $T$, by definition, $T$ is a $T_4$ space.
== Sources ==
* : Chapter $4$: Embedding and Metrization: Lemma $19$
Category:T3 Space with Sigma-Locally Finite Basis is T4 Space
T3 Space with Sigma-Locally Finite Basis is T4 Space/Proof 2

== Theorem ==
== Proof ==
From T3 Space with Sigma-Locally Finite Basis is Paracompact:
:$T$ is a paracompact space
From $T_3$ Space is Fully $T_4$ iff Paracompact:
:$T$ is a fully $T_4$ space.
From Fully $T_4$ Space is $T_4$ Space:
:$T$ is a $T_4$ space.
Category:T3 Space with Sigma-Locally Finite Basis is T4 Space
T4 Property Preserved in Closed Subspace

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space.
Let $T_K$ be a subspace of $T$ such that $K$ is closed in $T$.
If $T$ is a $T_4$ space then $T_K$ is also a $T_4$ space.
That is, the property of being a $T_4$ space is weakly hereditary.
=== Corollary ===
== Proof ==
Let $T = \struct {S, \tau}$ be a $T_4$ space.
Then:
:$\forall A, B \in \map \complement \tau, A \cap B = \O: \exists U, V \in \tau: A \subseteq U, B \subseteq V, U \cap V = \O$ 
That is, for any two disjoint closed sets $A, B \subseteq S$ there exist disjoint open sets $U, V \in \tau$ containing $A$ and $B$ respectively.
We have that the set $\tau_K$ is defined as:
:$\tau_K := \set {U \cap K: U \in \tau}$
where $K$ is closed in $T$.
Let $A, B \subseteq K$ be closed in $K$ such that:
:$A \cap B = \O$
From Intersection with Subset is Subset‎:
:$A \subseteq K \iff A \cap K = A$
As $K$ is itself closed in $T$, it follows that so is $A \cap K = A$ from Topology Defined by Closed Sets.
Similarly, so is $B \cap K = B$.
Because $T$ is a $T_4$ space:
:$\exists U, V \in \tau: A \subseteq U, B \subseteq V, U \cap V = \O$
As $A, B \subseteq K$:
:$A \subseteq U \cap K, B \subseteq V \cap K: \paren {U \cap K} \cap \paren {V \cap K} = \O$
From the definition of topological subspace, both $U \cap K$ and $V \cap K$ are open in $K$.
Thus the $T_4$ axiom is satisfied in $K$.
== Also see ==
* $T_4$ Property is not Hereditary.
The above proof hinges on the fact that as $K$ is closed in $T$, then $A \cap K = A$ and $B \cap K = B$ are also closed in $T$.
If $K$ is not closed in $T$, there is no such guarantee of closedness of $A$ and $B$.
== Sources ==
* : Part $\text I$: Basic Definitions: Section $2$: Separation Axioms: Functions, Products, and Subspaces
Category:Closed Sets
Category:T4 Spaces
Category:Topological Subspaces
T4 Property Preserved in Closed Subspace/Corollary

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space.
Let $T_K$ be a subspace of $T$ such that $K$ is closed in $T$.
If $T$ is a normal space then $T_K$ is also a normal space.
That is, the property of being a normal space is weakly hereditary.
== Proof ==
From the definition, $T = \struct {S, \tau}$ is a normal space :
:$\struct {S, \tau}$ is a $T_4$ space
:$\struct {S, \tau}$ is a $T_1$ (Fréchet) space.
From Separation Properties Preserved in Subspace, any subspace of a $T_1$ space is also a $T_1$ space.
From T4 Property Preserved in Closed Subspace, any closed subspace of a $T_4$ space is also a $T_4$ space.
Hence the result.
== Sources ==
* : Part $\text I$: Basic Definitions: Section $2$: Separation Axioms: Functions, Products, and Subspaces
Category:Closed Sets
Category:Normal Spaces
Category:Topological Subspaces
T4 Property is not Hereditary

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space which is a $T_4$ space.
Let $T_H = \struct {H, \tau_H}$, where $\O \subset H \subseteq S$, be a subspace of $T$.
Then it does not necessarily follow that $T_H$ is a $T_4$ space.
== Proof ==
Let $T$ be the Tychonoff plank.
Let $T'$ be the deleted Tychonoff plank.
By definition, $T'$ is a subspace of $T$.
From Tychonoff Plank is Normal, $T$ is a normal space.
From Deleted Tychonoff Plank is Not Normal, $T'$ is not a normal space.
Thus it is seen that the property of being a normal space is not inherited by a subspace.
Hence the result.
== Sources ==
* : Part $\text I$: Basic Definitions: Section $2$: Separation Axioms: Functions, Products, and Subspaces
Category:T4 Spaces
Category:Topological Subspaces
T4 Space is Preserved under Homeomorphism

== Theorem ==
Let $T_A = \struct {S_A, \tau_A}$ and $T_B = \struct {S_B, \tau_B}$ be topological spaces.
Let $\phi: T_A \to T_B$ be a homeomorphism.
If $T_A$ is a $T_4$ space, then so is $T_B$.
== Proof ==
Suppose that $T_A$ is a $T_4$ space.
Let $B_1$ and $B_2$ be closed in $T_B$ that are disjoint.
Denote by $A_1 := \phi^{-1} \sqbrk {B_1}$ and $A_2 := \phi^{-1} \sqbrk {B_2}$ the preimages of $B_1$ and $B_2$ under $\phi$, respectively.
From Preimage of Intersection under Mapping it follows that $A_1$ and $A_2$ are disjoint.
Also, as $\phi$ is a homeomorphism, it is a fortiori continuous.
Thus Continuity Defined from Closed Sets applies to yield that both $A_1$ and $A_2$ are closed.
Now as $T_A$ is a $T_4$ space, we find disjoint open sets $U_1$ containing $A_1$ and $U_2$ containing $A_2$.
From Image of Subset is Subset of Image, we have $B_1 = \phi \sqbrk {\phi^{-1} \sqbrk {B_1} } = \phi \sqbrk {A_1} \subseteq \phi \sqbrk {U_1}$.
Here, the first equality follows from Subset equals Image of Preimage iff Mapping is Surjection, as $\phi$ is a fortiori surjective, being a homeomorphism.
Then , we deduce also $B_2 \subseteq \phi \sqbrk {U_2}$.
From Image of Intersection under Injection it follows that $\phi \sqbrk {U_1}$ and $\phi \sqbrk {U_2}$ are disjoint.
Since $\phi$ is a homeomorphism, they are also both open in $T_B$.
Therewith, we have construed two disjoint open sets in $T_B$, one containing $B_1$, and the other containing $B_2$.
Hence $T_B$ is shown to be a $T_4$ space as well.
== Sources ==
* : Part $\text I$: Basic Definitions: Section $2$: Separation Axioms: Functions, Products, and Subspaces
Category:Homeomorphisms (Topological Spaces)
Category:T4 Spaces
T4 and T3 Space is T 3 1/2

== Theorem ==
Let $T = \struct {S, \tau}$ be:
:a $T_4$ space
and also:
:a $T_3$ space.
Then $T$ is also a $T_{3 \frac 1 2}$ space.
== Proof ==
Let $T = \struct {S, \tau}$ be a $T_4$ space which is also a $T_3$ space.
From it being $T_3$:
:$\forall F \subseteq S: \relcomp S F \in \tau, y \in \relcomp S F: \exists U, V \in \tau: F \subseteq U, y \in V: U \cap V = \O$
Consider this $U \in \tau$, which is disjoint from $\set y$.
Then $\relcomp S U$ is a closed set which is disjoint from $F$ but such that $\set y \subseteq \relcomp S U$.
As $T$ is a $T_4$ space, we have that from Urysohn's Lemma there exists an Urysohn function $f$ for $F$ and $\relcomp S U$.
As $\set y \subseteq \relcomp S U$, this function $f$ is a Urysohn function for $F$ and $\set y$ as well.
So:
:For any closed set $F \subseteq S$ and any point $y \in S$ such that $y \notin F$, there exists an Urysohn function for $F$ and $\set y$.
which is precisely the definition of a $T_{3 \frac 1 2}$ space.
== Sources ==
* : Part $\text I$: Basic Definitions: Section $2$: Separation Axioms: Completely Regular Spaces
Category:T4 Spaces
Category:T3 Spaces
Category:T3 1/2 Spaces
T5 Property is Hereditary

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space which is a $T_5$ space.
Let $T_H = \struct {H, \tau_H}$, where $\O \subset H \subseteq S$, be a subspace of $T$.
Then $T_H$ is a $T_5$ space.
== Proof ==
Let $T = \struct {S, \tau}$ be a $T_5$ space.
Then:
:$\forall A, B \subseteq S, \map {\cl_S} A \cap B = A \cap \map {\cl_S} B = \O: \exists U, V \in \tau: A \subseteq U, B \subseteq V, U \cap V = \O$ 
where $\map {\cl_S} A$ denotes the closure of $A$ in $S$.
That is:
:For any two separated sets $A, B \subseteq S$ there exist disjoint open sets $U, V \in \tau$ containing $A$ and $B$ respectively.
We have that the set $\tau_H$ is defined as:
:$\tau_H := \set {U \cap H: U \in \tau}$
Let $A, B \subseteq H$ such that $\map {\cl_H} A \cap B = A \cap \map {\cl_H} B = \O$.
That is, $A$ and $B$ are separated in $H$.
Then:
Similarly:
:$A \cap \map {\cl_S} B = \O$
So $A$ and $B$ are separated in $S$.
Because $T$ is a $T_5$ space, we have that:
:$\exists U, V \in \tau: A \subseteq U, B \subseteq V, U \cap V = \O$
It follows that:
:$\exists U \cap H, V \cap H \in \tau_H : A \subseteq U \cap H, B \subseteq V \cap H, \paren {U \cap H} \cap \paren {V \cap H} = \O$
and so the $T_5$ axiom is satisfied in $H$.
== Sources ==
* : Part $\text I$: Basic Definitions: Section $2$: Separation Axioms: Functions, Products, and Subspaces
Category:T5 Spaces
Category:Topological Subspaces
T5 Space iff Every Subspace is T4

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space.
Then $T$ is a $T_5$ space every subspace of $T$ is a $T_4$ space.
== Proof ==
=== Necessary Condition ===
Suppose $\struct {S, \tau}$ is $T_5$. 
Take an arbitrary subspace $\struct {Y, \tau_Y}$ of $S$. 
Let $A, B \subset Y$ be closed sets with $A \cap B = \O$. 
Let $R^-$ denote the closure of $R \subset Y$. 
From Closure of Subset in Subspace we have that:
:$\paren {A \cap Y}^- = A^- \cap Y$
But as $A \subseteq Y$ we have from Intersection with Subset is Subset‎ that $A \cap Y = A$, and so:
:$A^- = A^- \cap Y$
Since $A, B \subset S$, we look at $A^- \cap B$.
Since $A, B \subset Y$, we have: 
:$A^- \cap B = A^- \cap B \cap Y \subset A^- \cap Y = A^-$.
But from Closed Set Equals its Closure we have $A^- = A$, since $A$ is closed in $Y$.
Thus we obtain: 
:$A^- \cap B \subset A$ 
and similarly: 
:$A \cap B^- \subset B$ 
Since $A \cap B = \O$, we obtain:
:$A^- \cap B = \O$
and similarly:
:$A \cap B^- = \O$
Thus we now have:
:$A, B \subset S$
and:
:$A^- \cap B = B^- \cap A = \O$
Thus, since $S$ is $T_5$, there exist $U_0, U_1$ disjoint open sets in $S$, such that $A \subset U_0$ and $B \subset U_1$.
Then $V_i = U_i \cap Y$ is an open set in $Y$ for $i = 0, 1$.
Also:
:$V_0 \cap V_1 = \O$
and trivially:
:$A \subset V_0$
and:
:$B \subset V_1$
Thus $Y$ is $T_4$.
Since $Y \subset S$ was arbitrary, we have found that every subspace of $\struct {S, \tau}$ is $T_4$.
=== Sufficient Condition ===
Suppose every subspace of $\struct {S, \tau}$ is $T_4$.
Let $A, B \subset S$ with $A^- \cap B = B^- \cap A = \O$.
Then because every subspace of $\struct {S, \tau}$ is $T_4$, the subspace:
:$\struct {S \setminus \paren {A^- \cap B^-}, \tau_{S \setminus \paren {A^- \cap B^-} } }$
is $T_4$.
Because we have $A^- \cap B = B^- \cap A = \O$, from Set is Subset of its Topological Closure we see that:
:$A \cap B = \O$
Also:
:$A \subset S \setminus \paren {A^- \cap B^-}$
and:
:$B \subset S \setminus \paren {A^- \cap B^-}$
Then, because:
:$\struct {S \setminus \paren {A^- \cap B^-}, \tau_{S \setminus \paren {A^- \cap B^-} } }$
is $T_4$, there exist $U_0, U_1 \subset S \setminus \paren {A^- \cap B^-}$ disjoint open sets in $S \setminus \paren {A^- \cap B^-}$ such that $A \subset U_0$ and $B \subset U_1$. 
Because:
:$U_0 = V_0 \cap \paren {S \setminus \paren {A^- \cap B^-} }$ for some open set $V_0 \subset S$ in $S$
and similarly:
:$U_1 = V_1 \cap \paren {S \setminus \paren {A^- \cap B^-} }$ for some open set $V_1 \subset S$ in $S$
we find that:
:$A \subset V_0$
and:
:$B \subset V_1$
and:
:$V_0 \cap V_1 = \O$
Thus $\struct {S, \tau}$ is a $T_5$-space.
== Sources ==
* : Part $\text I$: Basic Definitions: Section $2$: Separation Axioms: Functions, Products, and Subspaces
Category:T5 Spaces
Category:T4 Spaces
Category:Topological Subspaces
T5 Space is Preserved under Homeomorphism

== Theorem ==
Let $T_A = \struct {S_A, \tau_A}$ and $T_B = \struct {S_B, \tau_B}$ be topological spaces.
Let $\phi: T_A \to T_B$ be a homeomorphism.
If $T_A$ is a $T_5$ space, then so is $T_B$.
== Proof ==
== Sources ==
* : Part $\text I$: Basic Definitions: Section $2$: Separation Axioms: Functions, Products, and Subspaces
Category:Homeomorphisms (Topological Spaces)
Category:T5 Spaces
T5 Space is T4 Space

== Theorem ==
Let $\struct {S, \tau}$ be a $T_5$ space.
Then $\struct {S, \tau}$ is also a $T_4$ space.
== Proof ==
Let $\struct {S, \tau}$ be a $T_5$ space.
From the definition of $T_5$ space:
:$\forall A, B \subseteq S, A^- \cap B = A \cap B^- = \O: \exists U, V \in \tau: A \subseteq U, B \subseteq V, U \cap V = \O$ 
where $A^-$ is the closure of $A$ in $T$.
Let $C, D \subseteq S$ be disjoint sets which are closed in $T$.
Thus $C, D \in \map \complement \tau$ from the definition of closed set.
From Topological Closure is Closed:
:$C^- = C, D^- = D$
and so from $C \cap D = \O$:
:$C^- \cap D = C \cap D^- = \O$
Thus from the definition of $T_5$ space:
:$\forall C, D \in \map \complement \tau, C \cap D = \O: \exists U, V \in \tau: C \subseteq U, D \subseteq V$ 
which is precisely the definition of a $T_4$ space.
== Sources ==
* : Part $\text I$: Basic Definitions: Section $2$: Separation Axioms
Category:T4 Spaces
Category:T5 Spaces
Tableau Confutation contains Finite Tableau Confutation

== Theorem == 
Let $\mathbf H$ be a countable set of WFFs of propositional logic.
Let $T$ be a tableau confutation of $\mathbf H$.
Then there exists a finite rooted subtree of $T'$ that is also a tableau confutation of $\mathbf H'$.
== Proof ==
For each node $v \in T$, let $\map p v$ be the path from $v$ to $r_T$, the root of $T$.
This path is unique by Path in Tree is Unique.
Let $\VV$ be the subtree of $T$ consisting those nodes $v$ of $T$ such that $\map p v$ is not contradictory.
 that $\VV$ were infinite.
Then by König's Tree Lemma, $\VV$ has an infinite branch $\Gamma$.
Since $\VV \subseteq T$, it follows that $\Gamma$ is also a branch of $T$.
However, by construction, it is impossible that $\Gamma$ is contradictory.
This contradicts that $T$ is a tableau confutation.
Hence $\VV$ is finite.
Next, define a finite propositional tableau $T'$ by:
:$v \in T' \iff \map \pi v \in \VV$
that is, the rooted tree formed by $\VV$ and all its children.
Then by construction, for each leaf node $v$ of $T'$, we have that $v \notin \VV$.
That is, that $\map p v$ is a contradictory branch of $T'$.
By Leaf of Rooted Tree is on One Branch, every branch of $T'$ is contradictory.
Hence $T'$ is a tableau confutation of $\mathbf H'$, as desired.
== Comment ==
Some sources define a tableau confutation to be a finite propositional tableau.
This result establishes that this distinction is not of material importance.
== Also see ==
* Definition:Tableau Confutation
Category:Propositional Tableaux
Tableau Confutation implies Unsatisfiable

== Theorem ==
Let $\mathbf H$ be a collection of WFFs of propositional logic.
Suppose there exists a tableau confutation of $\mathbf H$.
Then $\mathbf H$ is unsatisfiable for boolean interpretations.
== Proof ==
Let $\struct {T, \mathbf H, \Phi}$ be a tableau confutation of $\mathbf H$.
Suppose that $v$ were a boolean interpretation model for $\mathbf H$, that is:
:$v \models_{\mathrm{BI}} \mathbf H$
By Model of Root of Propositional Tableau is Model of Branch, it follows that:
:$v \models_{\mathrm{BI}} \Phi \sqbrk \Gamma$
for some branch $\Gamma$ of $T$.
Since $T$ is a tableau confutation, there is some WFF $\mathbf A$ such that:
:$\mathbf A, \neg\mathbf A \in \Phi \sqbrk \Gamma$
Hence $v \models_{\mathrm{BI}} \mathbf A$, that is:
:$\map v {\mathbf A} = T$
But by the truth table for $\neg$, this means:
:$\map v {\neg \mathbf A} = F$
which contradicts that $v \models_{\mathrm{BI}} \neg \mathbf A$.
Hence, no such boolean interpretation can exist.
That is, $\mathbf H$ is unsatisfiable for boolean interpretations.
== Sources ==
* : $\S 1.8$: Soundness: Lemma $1.8.2$
Category:Propositional Tableaux
Tableau Extension Lemma

== Lemma ==
Let $T$ be a finite propositional tableau.
Let its hypothesis set $\mathbf H$ be finite.
Then $T$ can be extended to a finished finite propositional tableau $T'$ which also has hypothesis set $\mathbf H$.
=== General Statement ===
== Proof ==
Let $\mathbf A$ be a WFF of propositional logic at a node $t$ such that:
* $\mathbf A$ is not a basic WFF;
* There is a non-contradictory branch through $t$ on which $\mathbf A$ is not used.
Such a WFF $\mathbf A$ will be called unused.
Note that a tableau is finished iff there are no unused WFFs in the tableau.
Let $u \left({T}\right)$ be the length of the longest unused WFF in $T$.
If $T$ is finished, we set $\map u T = 0$.
Since there are only finitely many WFFs in $T$, the number $\map u T$ must exist.
Let $\map R n$ be the proposition that every finite propositional tableau with hypothesis set $\mathbf H$ and with $\map u T < n$ can be extended to a finite finished tableau.
That is, $\map R n$ is an assertion that this lemma is true whenever $\map u T < n$.
The statement $\map R 1$ is true, because a tableau $T$ such that $\map u T < 1$ is already finished.
So, let us assume the truth of $\map R k$.
Suppose that $\map u T < k + 1$.
We extend $T$ to a new tableau $T'$ by using every unused WFF $\mathbf A$ in $T$ once on every non-contradictory branch through $\mathbf A$.
Each of the unused WFFs in $T$ is used in the new tableau $T'$.
Also, each new WFF which was added when forming $T'$ has a length less than $\map u T$, because the added WFFs are always shorter than the used WFFs.
So $\map u {T'} < \map u T < k + 1$, so $\map u {T'} < k$.
So, by the induction hypothesis $\map R k$, there is a finite finished extension $T' '$ of $T'$.
$T' '$ is also a finished extension of $T$.
Hence $\map R {k + 1}$, and the result follows by strong induction.
== Sources ==
* : $\S 1.10$: Completeness: Lemma $1.10.2$
Category:Tableau Extension Lemma
Category:Propositional Tableaux
Tableau Extension Lemma/General Statement

== Theorem ==
Let $T$ be a finite propositional tableau.
Let its hypothesis set $\mathbf H$ be finite.
Let $\mathbf H'$ be another finite set of WFFs.
Then there exists a finished finite propositional tableau $T'$ such that:
$(1):\quad$ the root of $T'$ is $\mathbf H \cup \mathbf H'$;
$(2):\quad$ $T$ is a rooted subtree of $T'$.
== Proof 1 ==
== Proof 2 ==
Category:Tableau Extension Lemma
Category:Propositional Tableaux
Tableau Extension Lemma/General Statement/Proof 1

== Theorem ==
Let $T$ be a finite propositional tableau.
Let its hypothesis set $\mathbf H$ be finite.
== Proof ==
Let $T_{\mathbf H'}$ be the finite propositional tableau obtained by replacing the hypothesis set $\mathbf H$ of $T$ with $\mathbf H \cup \mathbf H'$.
By the Tableau Extension Lemma, $T_{\mathbf H'}$ has a finished extension $T'$.
By definition of extension, $T_{\mathbf H'}$ is a rooted subtree of $T'$.
But $T_{\mathbf H'}$ and $T$ are equal when considered as rooted trees.
The result follows.
Category:Tableau Extension Lemma
Tac-Locus/Examples/Arbitrary Example 1

== Example of Tac-Locus ==
Let $\FF$ be the family of circles embedded in the Cartesian plane defined by the equation:
:$\paren {x - m}^2 + \paren {y - m}^2 = 4$
whose parameter is $m$.
The tac-locus of $\FF$ is the straight line whose equation is $y = x$.
== Sources ==
* 
* 
Category:Examples of Tac-Loci
Tac-Point/Examples/Arbitrary Example 1

== Example of Tac-Point ==
Let $\FF$ be the family of circles embedded in the Cartesian plane defined by the equation:
:$\paren {x - m}^2 + \paren {y - m}^2 = 4$
whose parameter is $m$.
The circle with $m = 0$ has its center at the origin.
The circle with $m = 2 \sqrt 2$ has its center at $\tuple {2 \sqrt 2, 2 \sqrt 2}$.
These two circles have a tac-point at $\tuple {\sqrt 2, \sqrt 2}$.
== Sources ==
* 
* 
Category:Examples of Tac-Points
Tail of Convergent Sequence

== Theorem ==
Let $\left\langle{a_n}\right\rangle$ be a real sequence.
Let $m \in \N$ be a natural number.
Let $a \in \R$ be a real number.
Then:
:$a_n \to a$
:
:$a_{n + m} \to a$
== Proof ==
=== Necessary Condition ===
Suppose that $a_n \to a$. 
Then for each $\epsilon > 0$, there exists $N \in \N$ such that: 
:$\size {a_n - a} < \epsilon$ for $n \ge N$. 
Set: 
:$N^\ast = \max \set {1, N - m}$ 
Then for $n \ge N^\ast$, we have $n \ge N - m$ and so $n + m \ge N$.
Then: 
:$\size {a_{n + m} - a} < \epsilon$ for $n \ge N^\ast$. 
So $a_{n + m} \to a$.
=== Sufficient Condition ===
Suppose that $a_{n + m} \to a$ for all $m \in \N$. 
Then in particular $a_{n + 1} \to a$. 
So for each $\epsilon > 0$ there exists $N \in \N$ such that: 
:$\size {a_{n + 1} - a} < \epsilon$ for $n \ge N$. 
Then: 
:$\size {a_n - a} < \epsilon$ for $n \ge N + 1$.
So $a_n \to a$.
Category:Convergence
Category:Sequences