Point is Isolated iff not Accumulation Point

Theorem

Let $T = \left({S, \tau}\right)$ be a topological space.

Let $H \subseteq S$.

Let $x \in H$.

Then:

$x$ is an isolated point in $H$

if and only if:

$x$ is not an accumulation point of $H$

Proof

Sufficient Condition

Let $x \in H$ be an isolated point in $H$.

Then by definition of isolated point:

$\exists U \in \tau: H \cap U = \left\{ {x}\right\}$

That is, by definition of Definition of uniqueness:

$\lnot \forall U \in \tau: \left({x \in U \implies \exists y \in S: \left({y \in H \cap U \land x \ne y}\right)}\right)$

Hence by Characterization of Derivative by Open Sets:

$x \notin A'$

where $A'$ denotes the derivative of $A$.

Thus by definition of derivative:

$x$ is not an accumulation point of $H$.

$\Box$

Necessary Condition

Let $x \in H$ not be an accumulation point of $H$.

Thus by definition of derivative:

$x \notin A'$

Hence:

\(\ds \lnot \forall U \in \tau\)

\(:\)

\(\ds \left({x \in U \implies \exists y \in S: \left({y \in H \cap U \land x \ne y}\right)}\right)\)

Characterization of Derivative by Open Sets

\(\ds \exists U \in \tau\)

\(:\)

\(\ds \lnot \left({x \in U \implies \exists y \in S: \left({y \in H \cap U \land x \ne y}\right)}\right)\)

Denial of Universality

\(\ds \exists U \in \tau\)

\(:\)

\(\ds \left({x \in U \land \lnot \exists y \in S: \left({y \in H \cap U \land x \ne y}\right)}\right)\)

Conjunction with Negative Equivalent to Negation of Implication

\(\ds \exists U \in \tau\)

\(:\)

\(\ds \left({x \in U \land \forall y \in S: \lnot \left({y \in H \cap U \land x \ne y}\right)}\right)\)

Denial of Existence

\(\ds \exists U \in \tau\)

\(:\)

\(\ds \left({x \in U \land \forall y \in S: \left({y \in H \cap U \implies x = y}\right)}\right)\)

Implication Equivalent to Negation of Conjunction with Negative

\(\ds \exists U \in \tau\)

\(:\)

\(\ds H \cap U = \left\{ {x}\right\}\)

Definition of Uniqueness, and $x \in H$

Thus by definition of isolated point:

$x$ is an isolated point in $H$.

$\blacksquare$