nyuuzyou/wikis huggingface dataset:
Sommerfeld-Watson Transform

== Theorem ==
Let $\map f z$ be a mapping with isolated poles.
Let $f$ go to zero faster than $\dfrac 1 {\size z}$ as $\size z \to \infty$.
Let $C$ be a contour that is deformed such that all poles of $\map f z$ are contained in $C$.
Then:
:$\ds \sum \limits_{n \mathop = -\infty}^\infty \paren {-1}^n \map f n = \frac 1 {2 i} \oint_C \frac {\map f z} {\sin \pi z} \rd z$
== Proof ==
From Cauchy's Residue Theorem:
This is for poles $z_k$ at order $N = 1$ because we say that simple poles exist for $\dfrac {\map f z} {\sin \pi z}$.
Using l'Hôpital's rule:
But $\sin \pi z$ has poles at $z_k = n$ for some $n \in \Z$ which implies:
Finally:
:$\dfrac 1 {\cos \pi n} = \cos \pi n = \paren {-1}^n$
Therefore:
:$\ds \frac 1 {2 i} \oint_C \map f z \rd z = \sum_{n \mathop = -\infty}^\infty \paren {-1}^n \map f n$
Category:Complex Analysis
Sophie Germain's Identity

== Theorem ==
For any two numbers $x$ and $y$:
:$x^4 + 4 y^4 = \paren {x^2 + 2 y^2 + 2 x y} \paren {x^2 + 2 y^2 - 2 x y}$
== Proof 1 ==
== Proof 2 ==
== Sources ==
* : $\S 2$: Special Products and Factors: $2.19$
* : $\S 2$: Special Products and Factors: $2.19.$
Category:Fourth Powers
Category:Sophie Germain's Identity
Sophie Germain Prime cannot be 6n+1

== Theorem ==
Let $p$ be a Sophie Germain prime.
Then $p$ cannot be of the form $6 n + 1$, where $n$ is a positive integer.
== Proof ==
Let $p$ be a Sophie Germain prime.
Then, by definition, $2 p + 1$ is prime.
 $p = 6 n + 1$ for some $n \in \Z_{>0}$.
Then:
and so $2 p + 1$ is not prime.
The result follows by Proof by Contradiction.
Category:Sophie Germain Primes
Sorgenfrey Line is Expansion of Real Line

== Theorem ==
Let $\R = \struct {\R, d}$ be the metric space defined in Real Number Line is Metric Space.
Let $T = \struct {\R, \tau}$ be the Sorgenfrey line.
Then $T$ is an expansion of $\R$ as a topological space.
== Proof ==
It is enough to prove that any open set in $\R$ is open in $T$.
Let $a, b \in \R$.
Then:
:$\ds \openint a b = \bigcup_{\epsilon \mathop > 0} \hointr {a + \epsilon} b$
Since $\hointr {a + \epsilon} b$ are open in $T$, $\openint a b$ is also open in $T$.
Category:Sorgenfrey Line
Sorgenfrey Line is First-Countable

== Theorem ==
Let $\R$ be the set of real numbers.
Let $\BB = \set {\hointr a b: a, b \in \R}$.
Let $\tau$ be the topology generated by $\BB$, that is, the Sorgenfrey line.
Then $\tau$ is first-countable.
== Proof ==
Let $\BB_x = \set {\hointr x {x + \dfrac 1 n} : n \in \N_{>0} }$.
We will show that:
:$(1): \quad \BB_x$ is countable
:$(2): \quad \BB_x$ is a local basis at $x$
$(1)$ follows from the fact that $\BB_x$ is a bijection from the set of natural numbers.
$(2)$ is demonstrated as follows:
By definition of local basis, it suffices to show that $\forall U \in \tau: x \in U: \exists B \in \BB_x: B \subseteq U$.
Pick any $U$ in $\tau$.
By definition of $\tau$, there exists $\hointr x {x + \epsilon} \subseteq U$ for some $\epsilon \in \R_{>0}$.
By the Axiom of Archimedes there exists $n \in \N$ such that $n > \dfrac 1 \epsilon$ (that is, $\dfrac 1 n < \epsilon$).
So:
:$x \in \hointr x {x + \dfrac 1 n} \subseteq \hointr x {x + \epsilon} \subseteq U$
Therefore $\BB_x$ is a local basis at $x$.
We have seen that the Sorgenfrey line has a countable local basis at every point.
By definition of first-countability, $\tau$ is first-countable.
== Also see ==
* Sorgenfrey Line is not Second-Countable
* Sorgenfrey Line is Separable
Category:Sorgenfrey Line
Sorgenfrey Line is Hausdorff

== Theorem ==
Let $T = \struct {\R, \tau}$ be the Sorgenfrey line.
Then $T$ is Hausdorff.
== Proof ==
Take $x, y \in \R$ such that $x \ne y$.
, assume that $x < y$.
From Real Numbers are Densely Ordered:
:$\exists t \in \R: x < t < y$
Then:
:$\hointr x t \cap \hointr t {y + 1} = \O$
We also have that $x \in \hointr x t$ by definition of half-open interval.
Also, as $t < y < y+1$ it is clear that $y \in \hointr t {y + 1}$.
By definition of the Sorgenfrey line, both are open in $T$.
Thus we have found two disjoint subsets of $\R$ which are open in $T$, such that one contains $x$ and the other contains $y$.
Hence the Sorgenfrey Line is Hausdorff by definition.
== Sources ==
* : Part $\text {II}$: Counterexamples: $51$. Right Half-Open Interval Topology: $2$
Category:Sorgenfrey Line
Category:Hausdorff Spaces
Sorgenfrey Line is Perfectly Normal

== Theorem ==
Let $T = \struct {\R, \tau}$ be the Sorgenfrey line.
Then $T$ is perfectly normal.
== Proof ==
From the definition of perfectly normal space, it is necessary to prove that $T$ is a $T_1$ space and that any closed set is $G_\delta$.
From $T_2$ Space is $T_1$ Space and Sorgenfrey Line is Hausdorff:
:the Sorgenfrey line is a $T_1$ space.
From Complement of $F_\sigma$ Set is $G_\delta$ Set it is sufficient to prove that an open set of $T$ is $F_\sigma$.
Let $W$ be any open set in $T$.
Let $O \subseteq W$ be the interior of $W$ with respect to the metric space:
:$\R = \struct {\R, d}$
where $d$ is the usual metric on $\R$.
From the definition of $T$, for each $x \in W \setminus O$, we can choose $h_x \in W$ such that $\hointr x {h_x} \subseteq W$.
Suppose $\hointr x {h_x} \cap \hointr y {h_y} \ne \O$ for some distinct points $x, y \in W \setminus O$.
Then either $x < y < h_x$ or $y < x < h_y$.
If $x < y < h_x$, then $y \in \openint x {h_x} \subseteq O$, contradicting $y \in W \setminus O$.
Similarly, if $y < x < h_y$, then $x \in \openint y {h_y}) \subseteq O$, contradicting $x \in W \setminus O$.
Thus $\family {\hointr x {h_x} }_{x \mathop \in W \setminus O}$ is a pairwise disjoint indexed family of open sets of $T$.
From Sorgenfrey Line is Separable and Separable Space satisfies Countable Chain Condition:
:$\set {\hointr x {h_x} : x \in W \setminus O}$ is countable
and thus:
:$W \setminus O$ is countable.
From Metric Space is Perfectly T4:
:$O$ is an $F_\sigma$ set in $\R$.
Thus from Sorgenfrey Line is Expansion of Real Line:
:$O$ is an $F_\sigma$ set in the Sorgenfrey line.
Since $W \setminus O$ is a countable union of singletons and $T$ is a $T_1$ space:
:$W \setminus O$ is an $F_\sigma$ set in $T$.
Since $W = O \cup \left({W \setminus O}\right)$ and $F_\sigma$ sets are closed under unions:
:$W$ is an $F_\sigma$ set in $T$.
Category:Sorgenfrey Line
Category:Perfectly Normal Spaces
Sorgenfrey Line is Separable

== Theorem ==
The Sorgenfrey line is separable.
== Proof ==
By Rationals are Everywhere Dense in Sorgenfrey Line:
:$\Q$ is dense in the Sorgenfrey line.
By Rational Numbers are Countably Infinite:
:$\Q$ is countable.
Thus by definition:
:The Sorgenfrey line is separable.
== Sources ==
* 
* 
Category:Sorgenfrey Line
Sorgenfrey Line is Topology

== Theorem ==
The Sorgenfrey Line is a topological space.
== Proof ==
We have to check that $\BB = \set {\hointr a b: a, b \in \R}$ fulfills the axioms of being a basis for a topology.
By definition of synthetic basis we only have to check that:
:$(1): \quad \bigcup \BB = \R$
:$(2): \quad \forall B_1, B_2 \in \BB: \exists V \in \BB: V \subseteq B_1 \cap B_2$
We have that:
:$\forall n \in \Z: \hointr n {n + 1} \in \BB$
:$\R = \ds \bigcup_{n \mathop \in \Z} \hointr n {n + 1} \subseteq \bigcup \BB$
Hence $\R = \bigcup \BB$ and condition $(1)$ is fulfilled.
Now take $ B_1, B_2 \in \BB$ where:
:$B_1 = \hointr {a_1} {b_1}$
:$B_2 = \hointr {a_2} {b_2}$
Let $B_3$ be constructed as:
:$B_3 := \hointr {\max \set {a_1, a_2} } {\min \set {b_1, b_2} } \in \BB$
From the method of construction, it is clear that $B_3 = B_1 \cap B_2$.
Thus taking $V = B_3$, condition $(2)$ is fulfilled.
== Sources ==
* : Part $\text {II}$: Counterexamples: $51$. Right Half-Open Interval Topology
Category:Sorgenfrey Line
Sorgenfrey Line is not Second-Countable

== Theorem ==
Let $T = \struct {\mathbb R, \tau}$ be the Sorgenfrey line.
Then $T$ is not second-countable.
== Proof ==
Suppose $\BB$ is a basis for $\tau$.
By definition of basis:
:$\forall U \in \tau: \forall x \in U: \exists B \in \BB: x \in B \subseteq U$
For all $x \in \R$, pick $U = \hointr x {x + \epsilon} \in \tau$ for some $\epsilon > 0$.
Now:
:$\forall x \in \R: \exists B_x \in \BB: x \in B_x \subseteq \hointr x {x + \epsilon}$
This $\BB_x$ has an infimum equal to $x$.
So for different $x$, the corresponding $\BB_x$ is different.
So the cardinality of $\BB$ is at least $\size \R$, which is uncountable.
== Also see ==
* Sorgenfrey Line is First-Countable
* Sorgenfrey Line is Separable
Category:Sorgenfrey Line
Sorgenfrey Line satisfies all Separation Axioms

== Theorem ==
Let $T = \left({\R, \tau}\right)$ be the Sorgenfrey line.
Then $T$ satisfies all separation axioms.
== Proof ==
We have Sorgenfrey Line is Perfectly Normal.
The result follows from Sequence of Implications of Separation Axioms.
Category:Sorgenfrey Line
Sorites/Examples/Heap of Sand

== Examples of Sorites ==
The archetypal example of a sorites, and in fact the one from which it got its name, is as follows:
:If you remove a grain of sand from a heap of sand, it remains a heap of sand.
:So, if you remove another grain of sand from that same heap of sand, it is still a heap of sand.
:And again, removing yet another grain of sand from that heap of sand, once again it stays a heap of sand.
:But at some stage you will have removed every grain of sand from that heap of sand except one.
:So is that grain of sand still a heap of sand?
== Sources ==
* 
Category:Examples of Sorites
Sound Proof System is Consistent

== Theorem ==
Let $\LL$ be a logical language.
Let $\mathscr M$ be a formal semantics for $\LL$.
Let $\mathscr P$ be a proof system for $\LL$.
Suppose that $\mathscr P$ is sound for $\mathscr M$.
Then $\mathscr P$ is consistent.
== Proof ==
By assumption, some logical formula $\phi$ is not an $\mathscr M$-tautology.
Since $\mathscr P$ is sound for $\mathscr M$, $\phi$ is also not a $\mathscr P$-theorem.
But then by definition $\mathscr P$ is consistent.
== Sources ==
* : $\S 4.4$: Conditions for an Axiom System: Theorem $1$
Category:Proof Systems
Soundness Theorem for Hilbert Proof System

== Theorem ==
Let $\mathscr H$ be instance 1 of a Hilbert proof system.
Let $\mathrm{BI}$ be the formal semantics of boolean interpretations.
Then $\mathscr H$ is a sound proof system for $\mathrm{BI}$:
:Every $\mathscr H$-theorem is a tautology.
== Proof ==
Recall the axioms of $\mathscr H$:
That these are tautologies is shown on, respectively:
:True Statement is implied by Every Statement
:Self-Distributive Law for Conditional
:Rule of Transposition
That Modus Ponens infers tautologies from tautologies is shown on:
:Modus Ponendo Ponens
Since:
:All axioms of $\mathscr H$ are tautologies;
:All rules of inference of $\mathscr H$ preserve tautologies
it is guaranteed that every formal proof in $\mathscr H$ results in a tautology.
That is, all $\mathscr H$-theorems are tautologies.
== Sources ==
* : $\S 3.6$: Theorem $3.37$
Category:Hilbert Proof System Instance 1
Soundness Theorem for Hilbert Proof System for Predicate Logic

== Theorem ==
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.
== Sources ==
* : $\text{II}.10$ Formal Proofs: Lemma $\text{II}.10.5$
Category:Soundness Theorem
Category:Hilbert Proof System Instance 1 for Predicate Logic
Soundness Theorem for Propositional Tableaux and Boolean Interpretations

== Theorem ==
Tableau proofs (in terms of propositional tableaux) are a sound proof system for boolean interpretations.
That is, for every WFF $\mathbf A$:
:$\vdash_{\mathrm{PT} } \mathbf A$ implies $\models_{\mathrm{BI} } \mathbf A$
== Proof ==
This is a corollary of the Extended Soundness Theorem for Propositional Tableaux and Boolean Interpretations:
Let $\mathbf H$ be a countable set of propositional formulas.
Let $\mathbf A$ be a propositional formula.
If $\mathbf H \vdash \mathbf A$, then $\mathbf H \models \mathbf A$.
In this case, we have $\mathbf H = \O$.
Hence the result.
== Also see ==
* Completeness Theorem for Propositional Tableaux and Boolean Interpretations in which it is proved that:
:If $\models \mathbf A$ then $\vdash \mathbf A$.
* Extended Soundness Theorem for Propositional Tableaux and Boolean Interpretations
== Sources ==
* : $\S 1.8$: Soundness
Category:Propositional Tableaux
Category:Named Theorems
Soundness Theorem for Semantic Tableaux

== Theorem ==
Let $\mathbf A$ be a WFF of propositional logic.
Let $T$ be a completed tableau for $\mathbf A$.
Suppose that $T$ is closed.
Then $\mathbf A$ is unsatisfiable for boolean interpretations.
== Proof ==
We will prove inductively the following claim for every node $t$ of $T$:
:If all leaves that are descendants of $t$ are marked closed, then $\map U t$ is unsatisfiable.
By the Semantic Tableau Algorithm, we know this statement to hold for the leaf nodes themselves.
For, a leaf $t$ is marked closed $\map U t$ contains a complementary pair.
The assertion follows from Set of Literals Satisfiable iff No Complementary Pairs.
Inductively, suppose that all children of a node $t$ satisfy the mentioned condition.
If all descendant leaf nodes of $t$ are marked closed, this evidently holds for the children $t', t' '$ of $t$ as well.
Hence by hypothesis, $\map U {t'}$ and $\map U {t' '}$ are unsatisfiable.
Let $\mathbf B$ be the WFF used by the Semantic Tableau Algorithm at $t$.
Let $\mathbf B_1, \mathbf B_2$ be the formulas added to $t'$ and $t' '$.
First, the case that $\mathbf B$ is an $\alpha$-formula.
Then $t' = t' '$, and $\mathbf B$ is semantically equivalent to $\mathbf B_1 \land \mathbf B_2$.
It follows that if:
:$v \models_{\mathrm{BI}} \map U t$
for some boolean interpretation $v$, then also:
:$v \models_{\mathrm{BI}} \map U {t'}$
which contradicts our hypothesis.
Thus, $\map U t$ is unsatisfiable.
Next, the case that $\mathbf B$ is a $\beta$-formula.
Then $\mathbf B$ is semantically equivalent to $\mathbf B_1 \lor \mathbf B_2$.
It follows that if:
:$v \models_{\mathrm{BI}} \map U t$
for some boolean interpretation $v$, then also one of the following must hold:
:$v \models_{\mathrm{BI}} \map U {t'}$
:$v \models_{\mathrm{BI}} \map U {t' '}$
which contradicts our hypothesis.
Thus, $\map U t$ is unsatisfiable.
This proves our claim:
:If all leaves that are descendants of $t$ are marked closed, then $\map U t$ is unsatisfiable.
Applying this claim to the root node of $T$, we obtain the desired result.
== Sources ==
* : $\S 2.7.1$
Category:Propositional Logic
Category:Named Theorems
Soundness and Completeness of Gentzen Proof System

== Theorem ==
Let $\mathscr G$ be instance 1 of a Gentzen proof system.
Let $\mathrm{BI}$ be the formal semantics of boolean interpretations.
Then $\mathscr G$ is a sound and complete proof system for $\mathrm{BI}$.
== Proof ==
This is an immediate consequence of:
* Provable by Gentzen Proof System iff Negation has Closed Tableau
* Soundness and Completeness of Semantic Tableaux
== Sources ==
* : $\S 3.2.1$: Theorem $3.8$
Category:Propositional Logic
Soundness and Completeness of Semantic Tableaux

== Theorem ==
Let $\mathbf A$ be a WFF of propositional logic.
Let $T$ be a completed semantic tableau for $\mathbf A$.
Then $\mathbf A$ is unsatisfiable $T$ is closed.
=== Corollary 1 ===
=== Corollary 2 ===
== Proof ==
The two directions of this theorem are respectively addressed on:
:Soundness Theorem for Semantic Tableaux
:Completeness Theorem for Semantic Tableaux
== Sources ==
* : $\S 2.7$: Theorem $2.67$
Category:Propositional Logic
Soundness and Completeness of Semantic Tableaux/Corollary 1

== Corollary to Soundness and Completeness of Semantic Tableaux ==
Let $\mathbf A$ be a WFF of propositional logic.
Let $T$ be a completed semantic tableau for $\mathbf A$.
Then $\mathbf A$ is satisfiable $T$ is open.
== Proof ==
$\mathbf A$ is satisfiable it is not unsatisfiable.
By the Soundness and Completeness of Semantic Tableaux, $\mathbf A$ is satisfiable $T$ is not closed.
Since $T$ is completed, this is the case $T$ is open.
== Sources ==
* : $\S 2.7$: Corollary $2.68$
Category:Propositional Logic
Soundness and Completeness of Semantic Tableaux/Corollary 2

== Corollary to Soundness and Completeness of Semantic Tableaux ==
Let $\mathbf A$ be a WFF of propositional logic.
Then $\mathbf A$ is a tautology $\neg \mathbf A$ has a closed tableau.
== Proof ==
By Tautology iff Negation is Unsatisfiable, $\mathbf A$ is a tautology $\neg \mathbf A$ is unsatisfiable.
By the Soundness and Completeness of Semantic Tableaux, this amounts to the existence of a closed tableau for $\neg \mathbf A$.
== Sources ==
* : $\S 2.7$: Corollary $2.69$
Category:Propositional Logic
Space in which All Convergent Sequences have Unique Limit not necessarily Hausdorff

== Theorem ==
Let $T = \struct{S, \tau}$ be a topological space.
Let $T$ be such that all convergent sequences have a unique limit.
Then it is not necessarily the case that $T$ is a Hausdorff space.
== Proof ==
Let $T = \struct{\R, \tau}$ be the set of real numbers $\R$ with the countable complement topology.
From Countable Complement Space is not $T_2$, $T$ is not a Hausdorff space.
Suppose $\sequence{x_n}$ is a sequence in $\R$ which converges to $x$.
Then $C = \set{x_n: x_n \ne x}$ is closed in $T$ because it is countable.
So $X \setminus C$ is a neighborhood of $x$.
This means there is some $N \in \N$ such that:
:$\forall n > N: x_n \in X \setminus C$
That is, $x_n = x$ for large $n$.
This means that if $x_n \to y$ then $y = x$, proving limits in $T$ are unique.
Category:Hausdorff Spaces
Category:Countable Complement Topology
Space is Compact iff exists Basis such that Every Cover has Finite Subcover

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space.
Then $T = \struct {S, \tau}$ is compact $\tau$ has a basis $\BB$ such that:
:from every cover of $S$ by elements of $\BB$, a finite subcover of $S$ can be selected.
== Proof ==
=== Sufficient Condition ===
Let every open cover for $S$ have a finite subcover.
Let $\BB$ be a basis $\BB$.
Then every cover of $S$ by elements of $\BB$ is an open cover for $S$.
So:
:from every cover of $S$ by elements of $\BB$, a finite subcover of $S$ can be selected.
=== Necessary Condition ===
Let $\tau$ have a basis $\BB$ such that:
:from every cover of $S$ by elements of $\BB$, a finite subcover of $S$ can be selected.
Let $\AA$ be an open cover of $S$.
Let $f: \AA \to \powerset B$ be the mapping defined by:
:$\forall A \in \AA : \map f A = \set{B \in \BB : B \subseteq A}$
Since each element of $\AA$ is open:
:$A = \bigcup \map f A$ for each $A \in \AA$.
Let $\AA' = \bigcup f \sqbrk {\AA}$.
Then $\AA'$ is an cover of $S$ by elements of $\BB$
By the premise, $\AA'$ has a finite subset $\FF'$ that covers $S$.
Let $g: \FF' \to \AA$ be the map each element of $\FF'$ to an element of $\AA$ that contains it.
Note that since $\FF'$ is finite, this does not require the Axiom of Choice.
Let $\FF = g \sqbrk {\FF'}$.
Then $\FF$ is a finite subcover of $\AA$.
It follows that every open cover of $S$ has a finite subcover of $S$.
</onlyinclude>
Category:Compact Spaces
Category:Subcovers
Category:Topological Bases
Space is First-Countable iff Character not greater than Aleph 0

== Theorem ==
Let $T$ be a topological space.
$T$ is first-countable :
:$\map \chi T \le \aleph_0$
where $\map \chi T$ denotes the character of $T$.
== Proof ==
=== Sufficient Condition ===
Let $T$ be first-countable.
By definition of first-countable:
:$\forall x \in T: \exists \BB \in \map {\mathbb B} x: \card \BB \le \aleph_0$
where $\map {\mathbb B} x$ denotes the set of all local bases at $x$.
Then by definition of character of a point:
:$\forall x \in T: \map \chi {x, T} \le \aleph_0$
Hence by definition of character of topogical space:
:$\map \chi T \le \aleph_0$
=== Necessary Condition ===
Let $\map \chi T \le \aleph_0$.
By definition of character of topogical space:
:$\forall x \in T: \map \chi {x, T} \le \aleph_0$
Then by definition of character of a point:
:$\forall x \in T: \exists \BB \in \map {\mathbb B} x: \card \BB \le \aleph_0$
Thus by definition of first-countable:
:$T$ is first-countable.
== Sources ==
* 
* 
Category:First-Countable Spaces‎
Space is Neighborhood of all its Points

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space.
Let $x \in S$.
Then $S$ is a neighborhood of $x$.
== Proof ==
By the definition of the topology $\tau$, $S$ is an open set.
From Set is Open iff Neighborhood of all its Points, $S$ is a neighborhood of $x$.
== Also see ==
* Set is Open iff Neighborhood of all its Points
Category:Neighborhoods
Space is Separable iff Density not greater than Aleph Zero

== Theorem ==
Let $T$ be a topological space.
Then:
:$T$ is separable $\map d T \le \aleph_0$
where
:$\map d T$ denotes the density of $T$,
:$\aleph$ denotes the aleph mapping.
== Proof ==
:$T$ is separable
:
:there exists a countable subset of $T$ which is dense by definition of separable space
:
:there exists a subset $A$ of $T$ such that $A$ is dense and exists an injection $A \to \N$ by definition of countable set
:
:there exists a subset $A$ of $T$ such that $A$ is dense and $\card A \le \card \N$ by Injection iff Cardinal Inequality
:
:there exists a subset $A$ of $T$ such that $A$ is dense and $\card A \le \aleph_0$ by Aleph Zero equals Cardinality of Naturals
:
:$\map d T \le \aleph_0$ by definition of density
where $\card A$ denotes the cardinality of $A$.
== Sources ==
* 
* 
Category:Denseness
Category:Separable Spaces
Space of Almost-Zero Sequences is Everywhere Dense in 2-Sequence Space

== Theorem ==
Let $\struct {\ell^2, \norm {\, \cdot \,}_2}$ be the 2-sequence space equipped with Euclidean norm.
Let $c_{00}$ be the space of almost-zero sequences.
Then $c_{00}$ is everywhere dense in $\struct {\ell^2, \norm {\, \cdot \,}_2}$
== Proof ==
Let $\mathbf x = \sequence {x_n}_{n \mathop \in \N} \in \ell^2$.
By definition of $\ell^2$:
:$\ds \sum_{i \mathop = 0}^\infty \size {x_i}^2 < \infty$
Let $\ds s_n := \sum_{i \mathop = 0}^n \size {x_i}^2$ be a sequence of partial sums of $\ds s = \sum_{i \mathop = 0}^\infty \size {x_i}^2$.
We have that $s$ is a convergent sequence:
:$\forall \epsilon \in \R_{>0}: \exists N \in \N: \forall n \in \N: n > N \implies \size {s_n - s} < \epsilon$
Note that:
Let $\ds N \in \N : \sum_{n \mathop = N + 1}^\infty \size {x_n}^2 < \epsilon^2$
Let $\mathbf y := \tuple {x_1 \ldots, x_N, 0, \ldots}$.
By definition, $\mathbf y \in c_{00}$.
We have that:
Hence by definition, $c_{00}$ is dense in $\ell^2$.
== Sources ==
* : $\S 1.3$: Normed and Banach spaces. Topology of normed spaces
Category:Normed Vector Spaces
Category:Denseness