avewright/proofwiki-math huggingface dataset:
Theorem: Sequence Characterization of Open Sets

Let $\struct {X, d}$ be a metric space.
Let $G \subseteq X$.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$G \subseteq X$ is an open set of $\struct {X, d}$}}
{{item|(2):|$\forall x \in G: \forall \sequence {x_n} \in X: x_n \to x: \exists n_0 \in \N: \forall n \ge n_0: \sequence {x_n} \in G$}}
{{end-itemize}}

Proof:
=== $(1)$ implies $(2)$ ===
Let $G \subseteq X$ be open in $\struct {X, d}$.
Let $x \in G$.
Let $\sequence {x_n}$ be a sequence in $X$ such that $x_n \to x$.
By definition of open set, there exists $\epsilon > 0$ such that:
: $B_\epsilon \left({x}\right) \subseteq G$
where $B_\epsilon \left({x}\right)$ is the open $\epsilon$-ball of $x$.
Since $x_n \to x$, there exists $n_0 \in \N$ such that:
: $\forall n \ge n_0: d \left({x_n, x}\right) < \epsilon$
Thus:
: $\forall n \ge n_0: x_n \in B_\epsilon \left({x}\right) \subseteq G$
{{qed|lemma}}
Theorem: Metric Space Continuity by Inverse of Mapping between Neighborhoods

Let $M_1 = \struct {A_1, d_1}$ and $M_2 = \struct {A_2, d_2}$ be metric spaces.
Let $f: A_1 \to A_2$ be a mapping from $A_1$ to $A_2$.
Let $a \in A_1$ be a point in $A_1$.
$f$ is continuous at $a$ with respect to the metrics $d_1$ and $d_2$ {{iff}}:
:for each neighborhood $N$ of $\map f a$ in $M_2$, $f^{-1} \sqbrk N$ is a neighborhood of $a$.

Proof:
By definition, $f$ is continuous at $a$ with respect to the metrics $d_1$ and $d_2$ {{iff}}:
:for each neighborhood $N$ of $\map f a$ in $M_2$ there exists a corresponding neighborhood $N'$ of $a$ in $M_1$ such that $f \sqbrk {N'} \subseteq N$.
For a mapping $f: X \to Y$ we have:
:$f \sqbrk U \subseteq V \iff U \subseteq f^{-1} \sqbrk V$
where $U \subseteq X$ and $V \subseteq Y$.
Hence the result.
{{qed}}
Theorem: Point in Metric Space has Neighborhood

Let $M = \struct {A, d}$ be a metric space.
Let $a \in A$ be a point in $M$.
Then there exists some neighborhood of $a$ in $M$.

Proof:
Let $a \in A$.
Then $A$ is a neighborhood of $a$ in $M$.
{{qed}}
Theorem: Point in Metric Space is Element of its Neighborhood

Let $N$ be a neighborhood of $a$ in $M$.
Then $a \in N$.

Proof:
Trivially follows by definition of neighborhood of $a$.
{{qed}}
Theorem: Superset of Neighborhood in Metric Space is Neighborhood

Let $N$ be a neighborhood of $a$ in $M$.
Let $N \subseteq N' \subseteq A$.
Then $N'$ is a neighborhood of $a$ in $M$.

Proof:
By definition of neighborhood:
:$\exists \epsilon \in \R_{>0}: \map {B_\epsilon} a \subseteq N$
where $\map {B_\epsilon} a$ is the open $\epsilon$-ball of $a$ in $M$.
By Subset Relation is Transitive:
:$\map {B_\epsilon} a \subseteq N'$
The result follows by definition of neighborhood of $a$.
{{qed}}
Theorem: Intersection of Neighborhoods in Metric Space is Neighborhood

Let $N, N'$ be neighborhoods of $a$ in $M$.
Then $N \cap N'$ is a neighborhood of $a$ in $M$.

Proof:
By definition of neighborhood:
:$\exists \epsilon_1 \in \R_{>0}: \map {B_{\epsilon_1} } a \subseteq N$
where $\map {B_{\epsilon_1} } a$ is the open $\epsilon_1$-ball of $a$ in $M$.
:$\exists \epsilon_2 \in \R_{>0}: \map {B_{\epsilon_2} } a \subseteq N'$
where $\map {B_{\epsilon_2} } a$ is the open $\epsilon_2$-ball of $a$ in $M$.
Thus by definition of intersection:
:$\map {B_\epsilon} a \subseteq N \cap N'$
where $\epsilon = \min \set {\epsilon_1, \epsilon_2}$
The result follows by definition of neighborhood of $a$.
{{qed}}
Theorem: Neighborhood in Metric Space has Subset Neighborhood

Let $N$ be a neighborhood of $a$ in $M$.
Then there exists a neighborhood $N'$ of $a$ such that:
:$(1): \quad N' \subseteq N$
:$(2): \quad N'$ is a neighborhood of each of its points.

Proof:
By definition of neighborhood:
:$\exists \epsilon \in \R_{>0}: \map {B_\epsilon} a \subseteq N$
By Open Ball is Neighborhood of all Points Inside, $N' = \map {B_\epsilon} a$ fulfils the conditions of the statement.
{{qed}}
Theorem: Basis for Element of Real Number Line

Let $M = \struct {\R, d}$ denote the real number line with the usual (Euclidean) metric.
Let $a \in \R$ be a point in $M$.
Then the set of all open intervals containing $a$ is a basis for the neighborhood system of $a$.

Proof:
Let $N$ be a neighborhood of $a$ in $M$.
Then by definition:
:$\exists \epsilon \in \R_{>0}: \map {B_\epsilon} a \subseteq N$
where $\map {B_\epsilon} a$ is the open $\epsilon$-ball at $a$.
The result follows from Open Ball in Real Number Line is Open Interval.
{{qed}}
Theorem: Open Ball in Real Number Line is Open Interval

Let $\struct {\R, d}$ denote the real number line $\R$ with the usual (Euclidean) metric $d$.
Let $x \in \R$ be a point in $\R$.
Let $\map {B_\epsilon} x$ be the open $\epsilon$-ball at $x$.
Then $\map {B_\epsilon} x$ is the open interval $\openint {x - \epsilon} {x + \epsilon}$.

Proof:
Let $S = \map {B_\epsilon} x$ be an open $\epsilon$-ball at $x$.
Let $y \in \map {B_\epsilon} x$.
Then:
{{begin-eqn}}
{{eqn | l = y
      | o = \in
      | m = \map {B_\epsilon} x
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \map d {y, x}
      | o = <
      | m = \epsilon
      | c = {{Defof|Open Ball of Metric Space|Open $\epsilon$-Ball}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \size {y - x}
      | o = <
      | m = \epsilon
      | c = {{Defof|Euclidean Metric on Real Number Line}}
}}
{{eqn | ll= \leadstoandfrom
      | l = -\epsilon
      | o = <
      | m = y - x
      | mo= <
      | r = \epsilon
      | c = {{Defof|Absolute Value}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x - \epsilon
      | o = <
      | m = y
      | mo= <
      | r = x + \epsilon
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = y
      | o = \in
      | m = \openint {x - \epsilon} {x + \epsilon}
      | c = {{Defof|Open Real Interval}}
}}
{{end-eqn}}
As the implications go both ways:
:$\map {B_\epsilon} x \subseteq \openint {x - \epsilon} {x + \epsilon}$
and
:$\map {B_\epsilon} x \supseteq \openint {x - \epsilon} {x + \epsilon}$
By definition of set equality:
:$\map {B_\epsilon} x = \openint {x - \epsilon} {x + \epsilon}$
Hence the result.
{{qed}}
Theorem: Open Real Interval is Open Ball

Let $\R$ denote the real number line with the usual (Euclidean) metric.
Let $I := \openint a b \subseteq \R$ be an open real interval.
Then $I$ is the open $\epsilon$-ball $\map {B_\epsilon} \alpha$ of some $\alpha \in \R$.

Proof:
Let:
{{begin-eqn}}
{{eqn | l = \alpha
      | r = \frac {a + b} 2
}}
{{eqn | l = \epsilon
      | r = \frac {b - a} 2
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = a
      | r = \alpha - \epsilon
}}
{{eqn | l = b
      | r = \alpha + \epsilon
}}
{{end-eqn}}
Thus:
:$\openint a b = \openint {\alpha - \epsilon} {\alpha + \epsilon}$
From Open Ball in Real Number Line is Open Interval:
:$\openint {\alpha - \epsilon} {\alpha + \epsilon} = \map {B_\epsilon} \alpha$
where $\map {B_\epsilon} \alpha$ is the open $\epsilon$-ball of $\alpha$ in $\R$.
Hence the result
{{qed}}
Theorem: Neighborhoods in Standard Discrete Metric Space

Let $M = \struct {A, d}$ be a metric space where $d$ is the standard discrete metric.
Let $a \in A$.
Then $\set a$ is a neighborhood of $a$ which forms a basis for the system of neighborhoods of $a$.

Proof:
By definition of the standard discrete metric:
:$\map d {x, y} = \begin {cases} 0 & : x = y  \\ 1 & : x \ne y \end {cases}$
Let $\epsilon \in \R_{>0}$ such that $\epsilon < 1$.
Then:
{{begin-eqn}}
{{eqn | l = \map {B_\epsilon} a
      | r = \set {x \in A: \map d {x, a} < \epsilon}
      | c = {{Defof|Open Ball|Open $\epsilon$-Ball of $a$}}
}}
{{eqn | ll= \leadsto
      | l = \map {B_\epsilon} a
      | r = \set a
      | c = 
}}
{{end-eqn}}
So by definition $\set a$ is a neighborhood of $a$.
Let $\NN_a$ be the system of neighborhoods of $a$.
Let $N \in \NN_a$ be a neighborhood of $a$.
Then:
{{begin-eqn}}
{{eqn | l = a
      | o = \in
      | r = N
      | c = Point in Metric Space is Element of its Neighborhood
}}
{{eqn | ll= \leadsto
      | l = \set a 
      | o = \subseteq
      | r = N
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {B_\epsilon} a
      | o = \subseteq
      | r = N
      | c = for all $\epsilon \in \R_{>0}$ such that $\epsilon < 1$
}}
{{end-eqn}}
Hence the result by definition of basis of a system of neighborhoods.
{{qed}}
Theorem: Subset of Standard Discrete Metric Space is Neighborhood of Each Point

Let $M = \struct {A, d}$ be a metric space where $d$ is the standard discrete metric.
Let $S \subseteq A$.
Let $a \in S$.
Then $S$ is a neighborhood of $a$.
That is, every subset of $A$ is a neighborhood of each of its points.

Proof:
Let $S \subseteq A$.
Let $a \in S$.
From Neighborhoods in Standard Discrete Metric Space, $\set a$ is a neighborhood of $a$.
As $a \in S$ it follows from Singleton of Element is Subset that $\set a \subseteq S$.
The result follows from Superset of Neighborhood in Metric Space is Neighborhood.
{{qed}}
Theorem: Continuity of Heaviside Step Function

Let $\mu_c: \R \to \R$ be the Heaviside step function:
:$\map {\mu_c} x = \begin {cases} 0 & : x < c \\ 1 & : x > c \\ \text {arbitrary} & : x = c \end {cases}$
Then $\mu_c$ is continuous at every point of $\R$ except at $c$.

Proof:
Let $x \in \R: x \ne c$.
Let $\epsilon \in \R_{>0}$.
Let $\delta < \size {x - c}$.
Then by definition of the Heaviside step function:
:$\forall y \in \closedint {x - \delta} {x + \delta}: \map {\mu_c} x = \begin {cases} 0 & : x < c \\ 1 & : x > c \end {cases}$
Thus:
:$\forall y \in \closedint {x - \delta} {x + \delta}: \map {\mu_c} y = \map {\mu_c} x$
Thus:
:$\size {y - x} \implies: \map {\mu_c} y - \map {\mu_c} x < \epsilon$
and so $\mu_c$ is continuous at $\R$ except at $x$.
{{qed|lemma}}
Now suppose $x = c$.
Let $\epsilon = \dfrac 1 3$.
Let $\delta \in \R_{>0}$.
Let $\alpha \in \R_{>0}: \alpha < \delta$.
Let $y = x + \alpha$.
Let $y \in \R: \size {y - x} < \delta$ and $y \ne x$.
Suppose $\map {\mu_c} y - \map {\mu_c} x < \epsilon$.
Then:
{{begin-eqn}}
{{eqn | l = y
      | r = x + \alpha
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {\mu_c} y
      | r = 1
      | c = 
}}
{{end-eqn}}
while:
{{begin-eqn}}
{{eqn | l = y
      | r = x - \alpha
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {\mu_c} y
      | r = 0
      | c = 
}}
{{end-eqn}}
So whatever the value of $\map f x$, either:
:$\map f {x + \alpha} - \map f x > \epsilon$
or:
:$\map f {x - \alpha} - \map f x > \epsilon$
It follows that $\mu_c$ is not continuous at $c$.
{{qed}}
Theorem: Metric Space Continuity by Neighborhood Basis

Let $M_1 = \struct {A_1, d_1}$ and $M_2 = \struct {A_2, d_2}$ be metric spaces.
Let $f: A_1 \to A_2$ be a mapping from $A_1$ to $A_2$.
Let $a \in A_1$ be a point in $A_1$.
Let $\BB_{\map f a}$ be a basis for the neighborhood system at $\map f a$.
$f$ is continuous at $a$ with respect to the metrics $d_1$ and $d_2$ {{iff}}:
:for each neighborhood $N$ in $\BB_{\map f a}$, $f^{-1} \sqbrk N$ is a neighborhood of $a$.

Proof:
By definition, $\BB_{\map f a}$ be a basis for the neighborhood system at $\map f a$ {{iff}}:
:$\forall N_a \subseteq M_2: \exists N \in \BB_{\map f a}: N \subseteq N_a$
where $N_a$ denotes a neighborhood of $\map f a$ in $M_2$.
Theorem: Closed Intervals form Neighborhood Basis in Real Number Line

Let $\R$ be the real number line with the usual (Euclidean) metric.
Let $a \in \R$ be a point in $\R$.
Let $\BB_a$ be defined as:
:$\BB_a := \set {\closedint {a - \epsilon} {a + \epsilon}: \epsilon \in \R_{>0} }$
that is, the set of all closed intervals of $\R$ with $a$ as a midpoint.
Then $\BB_a$ is a basis for the neighborhood system of $a$.

Proof:
Let $N$ be a neighborhood of $a$ in $M$.
Then by definition:
:$\exists \epsilon' \in \R_{>0}: \map {B_{\epsilon'} } a \subseteq N$
where $\map {B_{\epsilon'} } a$ is the open $\epsilon'$-ball at $a$.
From Open Ball in Real Number Line is Open Interval:
:$\map {B_{\epsilon'} } a = \openint {a - \epsilon'} {a + \epsilon'}$
Let $\epsilon \in \R_{>0}: \epsilon < \epsilon'$.
Then by definition of closed interval and open interval:
:$\closedint {a - \epsilon} {a + \epsilon} \subseteq \openint {a - \epsilon'} {a + \epsilon'}$
From Subset Relation is Transitive:
:$\closedint {a - \epsilon} {a + \epsilon} \subseteq N$
Also by definition of closed interval and open interval:
:$\openint {a - \epsilon} {a + \epsilon} \subseteq \closedint {a - \epsilon} {a + \epsilon}$
From Open Real Interval is Open Ball, $\openint {a - \epsilon} {a + \epsilon}$ is the open $\epsilon$-ball at $a$.
Thus by definition, $\closedint {a - \epsilon} {a + \epsilon}$ is a neighborhood of $a$ in $M$.
Hence there exists a neighborhood $\closedint {a - \epsilon} {a + \epsilon}$ of $a$ which is a subset of $N$.
Hence the result by definition of basis for the neighborhood system of $a$.
{{qed}}
Theorem: Open Rational-Number Balls form Neighborhood Basis in Real Number Line

Let $\R$ be the real number line with the usual (Euclidean) metric.
Let $a \in \R$ be a point in $\R$.
Let $\BB_a$ be defined as:
:$\BB_a := \set {\map {B_\epsilon} a: \epsilon \in \Q_{>0} }$
that is, the set of all open $\epsilon$-balls of $a$ for rational $\epsilon$.
Then the $\BB_a$ is a basis for the neighborhood system of $a$.

Proof:
Let $N$ be a neighborhood of $a$ in $M$.
Then by definition:
:$\exists \epsilon' \in \R_{>0}: \map {B_{\epsilon'} } a \subseteq N$
where $\map {B_{\epsilon'} } a$ is the open $\epsilon'$-ball at $a$.
From Open Ball in Real Number Line is Open Interval:
:$\map {B_{\epsilon'} } a = \openint {a - \epsilon'} {a + \epsilon'}$
From Between two Real Numbers exists Rational Number:
:$\exists \epsilon \in \Q: 0 < \epsilon < \epsilon'$
and so:
:$\openint {a - \epsilon} {a + \epsilon} \subseteq \openint {a - \epsilon'} {a + \epsilon'}$
From Open Real Interval is Open Ball
:$\map {B_\epsilon} a = \openint {a - \epsilon} {a + \epsilon}$
is the open $\epsilon$-ball at $a$.
From Subset Relation is Transitive:
:$\openint {a - \epsilon} {a + \epsilon} \subseteq N$
From Open Ball is Neighborhood of all Points Inside, $\openint {a - \epsilon} {a + \epsilon}$ is a neighborhood of $a$ in $M$.
Hence there exists a neighborhood $\openint {a - \epsilon} {a + \epsilon}$ of $a$ which is a subset of $N$.
Hence the result by definition of basis for the neighborhood system of $a$.
{{qed}}
Theorem: Open Reciprocal-N Balls form Neighborhood Basis in Real Number Line

Let $\R$ denote the real number line with the usual (Euclidean) metric.
Let $a \in \R$ be a point in $\R$.
Let $\BB_a$ be defined as:
:$\BB_a := \set {\map {B_\epsilon} a: \epsilon \in \set {\dfrac 1 n: n \in \N} }$
that is, the set of all open $\epsilon$-balls of $a$ for $\epsilon$ which are reciprocals of integers.
Then $\BB_a$ is a basis for the neighborhood system of $a$.

Proof:
Let $N$ be a neighborhood of $a$ in $M$.
Then by definition:
:$\exists \epsilon' \in \R_{>0}: \map {B_{\epsilon'} } a \subseteq N$
where $\map {B_{\epsilon'} } a$ is the open $\epsilon'$-ball at $a$.
From Open Ball in Real Number Line is Open Interval:
:$\map {B_{\epsilon'} } a = \openint {a - \epsilon'} {a + \epsilon'}$
From Between two Real Numbers exists Rational Number:
:$\exists \epsilon'' \in \Q: 0 < \epsilon'' < \epsilon'$
Let $\epsilon''$ be expressed in canonical form:
:$\epsilon'' = \dfrac p q$
Let $\epsilon = \dfrac 1 q$
Then $\epsilon \le \epsilon'' < \epsilon'$
and so:
:$\openint {a - \epsilon} {a + \epsilon} \subseteq \openint {a - \epsilon'} {a + \epsilon'}$
From Open Real Interval is Open Ball
:$\map {B_\epsilon} a = \openint {a - \epsilon} {a + \epsilon}$
is the open $\epsilon$-ball at $a$.
From Subset Relation is Transitive:
:$\openint {a - \epsilon} {a + \epsilon} \subseteq N$
From Open Ball is Neighborhood of all Points Inside, $\openint {a - \epsilon} {a + \epsilon}$ is a neighborhood of $a$ in $M$.
Hence there exists a neighborhood $\openint {a - \epsilon} {a + \epsilon}$ of $a$ which is a subset of $N$.
Hence the result by definition of basis for the neighborhood system of $a$.
{{qed}}
Theorem: Subset of Open Reciprocal-N Balls forms Neighborhood Basis in Real Number Line

Let $\R$ denote the real number line with the usual (Euclidean) metric.
Let $a \in \R$ be a point in $\R$.
Let $k \in \Z$ be some fixed integer.
Let $\BB_a$ be defined as:
:$\BB_a := \set {\map {B_\epsilon} a: \epsilon \in \set {\dfrac 1 n: n \in \N, n > k} }$
that is, the set of all open $\epsilon$-balls of $a$ for $\epsilon$ which are reciprocals of integers greater than $k$.
Then the $\BB_a$ is a basis for the neighborhood system of $a$.

Proof:
Let $N$ be a neighborhood of $a$ in $M$.
Then by definition:
:$\exists \epsilon' \in \R_{>0}: \map {B_{\epsilon'} } a \subseteq N$
where $\map {B_{\epsilon'} } a$ is the open $\epsilon'$-ball at $a$.
From Open Ball in Real Number Line is Open Interval:
:$\map {B_{\epsilon'} } a = \openint {a - \epsilon'} {a + \epsilon'}$
From Between two Real Numbers exists Rational Number:
:$\exists \epsilon'' \in \Q: 0 < \epsilon'' < \epsilon'$
Let $\epsilon''$ be expressed in canonical form:
:$\epsilon'' = \dfrac p q$
Let $\epsilon''' = \dfrac 1 q$
Then $\epsilon''' \le \epsilon'' < \epsilon'$
If $q \le k$, let $\epsilon = \dfrac 1 {k + 1}$
Otherwise, let $\epsilon = \epsilon'''$.
Then:
:$\openint {a - \epsilon} {a + \epsilon} \subseteq \openint {a - \epsilon'} {a + \epsilon'}$
From Open Real Interval is Open Ball
:$\map {B_\epsilon} a = \openint {a - \epsilon} {a + \epsilon}$
is the open $\epsilon$-ball at $a$.
By its method of construction:
:$\map {B_\epsilon} a \in \set {\map {B_\epsilon} a: \epsilon \in \set {\dfrac 1 n: n \in \N, n > k} }$
From Subset Relation is Transitive:
:$\openint {a - \epsilon} {a + \epsilon} \subseteq N$
From Open Ball is Neighborhood of all Points Inside, $\openint {a - \epsilon} {a + \epsilon}$ is a neighborhood of $a$ in $M$.
Hence the result by definition of basis for the neighborhood system of $a$.
{{qed}}
Theorem: Neighborhood Basis in Real Number Line is Infinite

Let $\R$ be the real number line with the usual (Euclidean) metric.
Let $a \in \R$ be a point in $\R$.
Let $\BB_a$ be a basis for the neighborhood system of $a$.
Then $\BB_a$ is an infinite set.

Proof:
{{AimForCont}} $\BB_a$ be finite.
Let the elements of $\BB_a$ be enumerated as $N_1, N_2, \ldots, N_n$.
For each $N_k \in \BB_a$, let $\map {B_{\epsilon_k} } a$ be the open $\epsilon_k$-ball of $a$ for some $\epsilon_k \in \R_{>0}$.
Let $\alpha = \min \set {\epsilon_k: k \in \set {1, 2, \ldots, n} }$.
Consider the open interval:
:$I = \openint {a - \beta} {a + \beta}$
where $\beta = \dfrac \alpha 2$
By the method of construction of $I$, it follows that $\map {B_{\epsilon_k} } a \nsubseteq I$ for any $k$.
Thus $I$ is a neighborhood of $a$ which does not have an element of $\BB_a$ as a subset.
So $\BB_a$ cannot be a basis for the neighborhood system of $a$.
Hence the result.
{{qed}}
Theorem: Distinct Points in Metric Space have Disjoint Neighborhoods

Let $M = \struct {A, d}$ be a metric space.
Let $x, y \in M: x \ne y$.
Then there exist neighborhoods $N_x$ and $N_y$ of $x$ and $y$ respectively such that $N_x \cap N_y = \O$, that is, that are disjoint.

Proof:
Let $x, y \in A: x \ne y$.
From Distinct Points in Metric Space have Disjoint Open Balls, there exist disjoint open $\epsilon$-balls $\map {B_\epsilon} x$ and $\map {B_\epsilon} y$ containing $x$ and $y$ respectively.
From Open Ball is Neighborhood of all Points Inside it follows that $\map {B_\epsilon} x$ and $\map {B_\epsilon} y$ are neighborhoods of $x$ and $y$ respectively.
Hence the result.
{{qed}}
Theorem: Point in Metric Space has Countable Neighborhood Basis

Let $M = \struct {A, d}$ be a metric space.
Let $a \in A$.
Then there exists a basis for the neighborhood system of $a$ which is countable.

Proof:
Consider the countable set:
:$\BB_a := \set {\map {B_\epsilon} a: \exists n \in \Z_{>0}: \epsilon = \dfrac 1 n}$
That is, let $\BB_a$ be the set of all open $\epsilon$-balls of $a$ such that $\epsilon$ is of the form $\dfrac 1 n$ for (strictly) positive integral $n$.
Let $N$ be a neighborhood of $a$.
Then by definition of neighborhood:
:$\exists \epsilon' \in \R_{>0}: \map {B_{\epsilon'} } a \subseteq N$
From Between two Real Numbers exists Rational Number:
:$\exists \epsilon'' \in \Q: 0 < \epsilon'' < \epsilon'$
Let $\epsilon''$ be expressed in canonical form as:
:$\epsilon'' = \dfrac p q$
where $p$ and $q$ are coprime integers and $q > 0$.
Then:
:$\epsilon := \dfrac 1 q \le \dfrac p q$
Thus $0 < \epsilon < \epsilon'$.
So:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \map {B_\epsilon} a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map d {x, a}
      | o = < 
      | r = \epsilon
      | c = {{Defof|Open Ball of Metric Space}}
}}
{{eqn | ll= \leadsto
      | l = \map d {x, a}
      | o = < 
      | r = \epsilon'
      | c = as $\epsilon < \epsilon'$
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in 
      | r = \map {B_{\epsilon'} } a
      | c = {{Defof|Open Ball of Metric Space}}
}}
{{eqn | ll= \leadsto
      | l = \map {B_\epsilon} a
      | o = \subseteq 
      | r = \map {B_{\epsilon'} } a
      | c = {{Defof|Subset}}
}}
{{eqn | ll= \leadsto
      | l = \map {B_\epsilon} a
      | o = \subseteq 
      | r = N
      | c = Subset Relation is Transitive
}}
{{end-eqn}}
From Open Ball is Neighborhood of all Points Inside, $\map {B_\epsilon} a$ is a neighborhood of $a$.
But as $\epsilon = \dfrac 1 q$ where $q \in \Z_{>0}$ it follows that:
:$\map {B_\epsilon} a \in \set {\map {B_\epsilon} a: \exists n \in \Z_{>0}: \epsilon = \dfrac 1 n}$
Hence the result.
{{qed}}
Theorem: Neighborhood Basis in Cartesian Product under Chebyshev Distance

Let $M_1 = \struct {A_1, d_1}, M_2 = \struct {A_2, d_2}, \ldots, M_n = \struct {A_n, d_n}$ be metric spaces.
Let $\ds \AA = \prod_{i \mathop = 1}^n A_i$ be the cartesian product of $A_1, A_2, \ldots, A_n$.
Let $d_\infty: \AA \times \AA \to \R$ be the Chebyshev distance on $\AA$:
:$\ds \map {d_\infty} {x, y} = \max_{i \mathop = 1}^n \set {\map {d_i} {x_i, y_i} }$
where $x = \tuple {x_1, x_2, \ldots, x_n}, y = \tuple {y_1, y_2, \ldots, y_n} \in \AA$.
Let $a = \tuple {a_1, a_2, \ldots, a_n} \in \AA$.
For all $i \in \set {1, 2, \ldots, n}$, let $\BB_{a_i}$ be a basis for the system of neighborhoods for $a_i$ in $M_i$.
Let $\BB_a$ be the cartesian product of $\BB_{a_1}, \BB_{a_2}, \ldots, \BB_{a_n}$:
:$\ds \BB_a = \prod_{i \mathop = 1}^n \BB_{a_i}$
Then $\BB_a$ is a basis for the system of neighborhoods for $a$ in $M$.

Proof:
Let $N$ be a neighborhood of $a$ in $M$.
Then by definition of neighborhood:
:$\exists \epsilon \in \R_{>0}: \map {B_\epsilon} {a; d_\infty} \subseteq N$
where $\map {B_\epsilon} {a; d_\infty}$ is the open $\epsilon$-ball of $a$ under $d_\infty$.
From Open Ball in Cartesian Product under Chebyshev Distance:
:$\ds \map {B_\epsilon} {a; d_\infty} = \prod_{i \mathop = 1}^n \map {B_\epsilon} {a_i; d_i}$
From Open Ball is Neighborhood of all Points Inside, each $\map {B_\epsilon} {a_i; d_i}$ is a neighborhood of $a_i$.
By definition of basis for system of neighborhoods:
:$\exists N_i \in \BB_{a_i}: N_i \subseteq \map {B_\epsilon} {a_i; d_i}$
From Cartesian Product of Subsets:
:$\ds \prod_{i \mathop = 1}^n N_i \subseteq \prod_{i \mathop = 1}^n \map {B_\epsilon} {a_i; d_i} \subseteq N$
But $\ds \prod_{i \mathop = 1}^n N_i \in \BB_a = \prod_{i \mathop = 1}^n \BB_{a_i}$
Hence the result by definition of basis for system of neighborhoods.
{{qed}}