Characterization of Derivative by Open Sets
Theorem
Let $T = \struct {S, \tau}$ be a topological space.
Let $A$ be a subset of $T$.
Let $x$ be a point of $T$.
Then
- $x \in A'$
- for every open set $U$ of $T$:
- if $x \in U$
- then there exists a point $y$ of $T$ such that $y \in A \cap U$ and $x \ne y$
where
- $A'$ denotes the derivative of $A$.
Proof
Sufficient Condition
Let $x \in A'$.
Then $x$ is an accumulation point of $A$ by Definition:Set Derivative.
Then by definition of accumulation point:
- $(1): \quad x \in \paren {A \setminus \set x}^-$
where $A^-$ denotes the closure of $A$.
Let $U$ be an open set of $T$.
Let $x \in U$.
Then by $(1)$ and Condition for Point being in Closure:
- $\paren {A \setminus \set x} \cap U \ne \O$
Then there exists $y$ being a point such that:
- $(2): \quad y \in A \setminus \set x$ and $y \in U$.
Then $y \in A$ and $y \notin \set x$ by definition of set difference.
Hence by $(2)$ and the definitions of set intersection and singleton:
- $y \in A \cap U$ and $x \ne y$
$\Box$
Necessary Condition
Let $x$ be such that:
- $(3): \quad$ for every open set $U$ of $T$ if $x \in U$, then there exists a point $y$ of $T$ such that $y \in A \cap U$ and $x \ne y$.
It will be proved that:
- for every open set $G$ of $T$:
- if $x \in G$
- then $\paren {A \setminus \set x} \cap U \ne \O$.
Let $G$ be an open set of $T$ such that $x \in G$.
Then by $(3)$ there exists a point $y$ of $T$ such that:
- $(4): \quad y \in A \cap G$ and $x \ne y$
Then by the definitions of set intersection and singleton:
- $y \in A$ and $y \notin \set x$
By definition of set difference:
- $y \in A \setminus \set x$
By $(4)$ and the definition of set intersection:
- $y \in G$
Hence:
- $\paren {A \setminus \set x} \cap U \ne \O$
$\Box$
Then by Condition for Point being in Closure:
- $x \in \paren {A \setminus \set x}^-$
Then, by definition, $x$ is an accumulation point of $A$.
Hence by definition of set derivative:
- $x \in A'$
$\blacksquare$
Sources
- Mizar article TOPGEN_1:17