# Derivative is Included in Closure

Jump to navigation
Jump to search

## Theorem

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

Let $A$ be a subset of $S$.

Then

- $A' \subseteq A^-$

where

- $A'$ denotes the derivative of $A$
- $A^-$ denotes the closure of $A$.

## Proof

Let $x \in A'$.

By Condition for Point being in Closure it is enough to prove that:

- for every open set $G$ of $T$:
- if $x \in G$
- then $A \cap G \ne \varnothing$.

Let $G$ be an open set of $T$.

Let $x \in G$.

Then by Characterization of Derivative by Open Sets:

- there exists a point $\exists y \in S: y \in A \cap G \land x \ne y$.

Hence:

- $A \cap G \ne \varnothing$

Hence the result.

$\blacksquare$

## Sources

- Mizar article TOPGEN_1:29