Derivative of Derivative is Subset of Derivative in T1 Space
Theorem
Let $T = \left({S, \tau}\right)$ be a $T_1$ topological space.
Let $A$ be a subset of $S$.
Then
- $A'' \subseteq A'$
where
- $A'$ denotes the derivative of $A$
Proof
Let:
- $(1): \quad x \in A''$.
Aiming for a contradiction, suppose that $x \notin A'$.
Then by Characterization of Derivative by Open Sets there exists an open subset $G$ of $T$ such that:
- $(2): \quad x \in G$ and
- $(3): \quad \lnot \exists y: y \in A \cap G \land x \ne y$.
By definition of $T_1$ space:
- $\left\{{x}\right\}$ is closed.
Then by Open Set minus Closed Set is Open:
- $(4): \quad G \setminus \{x\}$ is open.
By $(1)$, $(2)$, and Characterization of Derivative by Open Sets there exists a point $y$ of $T$ such that:
- $(5): \quad y \in A' \cap G$ and
- $(6): \quad x \ne y$.
Then by definition of intersection:
- $y \in A'$.
Then by $(6)$ and definition of set difference:
- $(7): \quad y \in A' \setminus \{x\}$.
By definition of intersection and $(5)$:
- $y \in G$.
By $(6)$ and definition of singleton:
- $y \notin \left\{{x}\right\}$
Then by definition of set difference:
- $(8): \quad y \in G \setminus \{x\}$
We will prove:
- $(9): \quad G \cap \left({A \setminus \{x\}}\right) = \varnothing$
- Aiming for a contradiction suppose that:
- $G \cap \left({A \setminus \left\{{x}\right\}}\right) \ne \varnothing$.
- Then by definition of the empty set there exists $g$ such that:
- $g \in G \cap \left({A \setminus \left\{{x}\right\}}\right)$
- Hence by definition of intersection:
- $g \in G$ and
- $g \in A \setminus \left\{{x}\right\}$.
- Then by definition of set difference:
- $g \in A$
- Hence by definition of intersection:
- $g \in A \cap G$
- Then by $(3)$:
- $x = g$
- Hence this by definition of singleton contadicts with $g \notin \left\{{x}\right\}$ obtained by definition of set difference.
- Thus $G \cap \left({A \setminus \left\{{x}\right\}}\right) = \varnothing$.
Define $U = G \setminus \{x\}$ as an open set by $(4)$.
By $(5)$ and definition of set difference:
- $y \in A'$
Then by $(8)$ and Characterization of Derivative by Open Sets there exists a point $q$ of $T$ such that
- $(10): \quad q \in A \cap U$ and
- $(11): \quad y \ne q$.
By $(10)$ and definition of intersection:
- $q \in A$
By $(11)$ and definition of singleton:
- $q \notin \left\{{y}\right\}$
Then by definition of set difference
- $(12): \quad q \in A \setminus \left\{{y}\right\}$.
By definition of intersection:
- $q \in U$.
Then by $(12)$ and by definition of set difference
- $q \ne x$ and $q \in A$.
Then by definition of set difference:
- $q \in A \setminus \{x\}$
and
- $q \in G$.
Hence this contradicts with $(9)$ by definition of intersection.
Thus the result by Proof by Contradiction.
$\blacksquare$
Sources
- Mizar article TOPGEN_1:32