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

Let $T = \struct {S, \tau}$ be a topological space.
Let $A$ be a subset of $S$.
Let $x$ be a point of $T$.
Let $A^-$ denote the closure of $A$.
Then $x \in A^-$ {{iff}}:
:for every open set $U$ of $T$:
::$x \in U \implies A \cap U \ne \O$

Proof:
=== Sufficient Condition ===
Let $x \in A^-$.
{{AimForCont}} there exists an open set $U$ of $T$ such that:
:$x \in U$ and $A \cap U = \O$
We have that $U$ is open in $T$.
So by definition of closed set, $\relcomp S U$ is closed in $T$.
Then:
{{begin-eqn}}
{{eqn | l = A \cap U
      | r = \O
      | c = 
}}
{{eqn | ll= \leadsto
      | l = A
      | o = \subseteq
      | r = \relcomp S U
      | c = Empty Intersection iff Subset of Complement
}}
{{eqn | ll= \leadsto
      | l = A^-
      | o = \subseteq
      | r = \relcomp S U
      | c = {{Defof|Closure (Topology)|index = 3}}: $\relcomp S U$ is closed
}}
{{eqn | ll= \leadsto
      | l = A^- \cap U
      | r = \O
      | c = Empty Intersection iff Subset of Complement
}}
{{end-eqn}}
But we have:
:$x \in A^-$
and also:
:$x \in U$
and thus by definition of set intersection:
:$x \in A^- \cap U$
This contradicts $A^- \cap U = \O$
Hence by Proof by Contradiction the assumption that there exists an open set $U$ of $T$ such that $x \in U$ and $A \cap U = \O$ was false.
So for every open set $U$ of $T$:
:$x \in U \implies A \cap U \ne \O$
{{qed|lemma}}
Theorem: Summation is Linear/Sum of Summations

:$\ds \sum_{i \mathop = 1}^n x_i + \sum_{i \mathop = 1}^n y_i = \sum_{i \mathop = 1}^n \paren {x_i + y_i}$

Proof:
The proof proceeds by mathematical induction.
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$\ds \sum_{i \mathop = 1}^n x_i + \sum_{i \mathop = 1}^n y_i = \sum_{i \mathop = 1}^n \paren {x_i + y_i}$
Theorem: Summation is Linear/Scaling of Summations

:$\ds \lambda \sum_{i \mathop = 1}^n x_i = \sum_{i \mathop = 1}^n \lambda x_i$

Proof:
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$\ds \lambda \sum_{i \mathop = 1}^n x_i = \sum_{i \mathop = 1}^n \lambda x_i$
Theorem: Supremum of Absolute Value of Difference equals Difference between Supremum and Infimum

Let $f$ be a real function.
Let $S$ be a subset of the domain of $f$.
Let $\ds \sup_{x \mathop \in S} \set {\map f x}$ and $\ds \inf_{x \mathop \in S} \set {\map f x}$ exist.
Then $\ds \sup_{x, y \mathop \in S} \set {\size {\map f x - \map f y} }$ exists and:
:$\ds \sup_{x, y \mathop \in S} \set {\size {\map f x - \map f y} } = \sup_{x \mathop \in S} \set {\map f x} - \inf_{x \mathop \in S} \set {\map f x}$

Proof:
{{begin-eqn}}
{{eqn | l = \sup_{x \mathop \in S} \set {\map f x} - \inf_{x \mathop \in S} \set {\map f x}
      | r = \sup_{x \mathop \in S} \set {\map f x} + \sup_{x \mathop \in S} \set {-\map f x}
      | c = Negative of Infimum is Supremum of Negatives
}}
{{eqn | r = \sup_{x, y \mathop \in S} \set {\map f x + \paren {-\map f y} }
      | c = Supremum of Sum equals Sum of Suprema
}}
{{eqn | r = \sup_{x, y \mathop \in S} \set {\map f x - \map f y}
}}
{{eqn | r = \sup_{x, y \mathop \in S} \set {\size {\map f x - \map f y} }
      | c = Supremum of Absolute Value of Difference equals Supremum of Difference
}}
{{end-eqn}}
{{qed}}
Category:Real Analysis
flxwxfp7d3e0cjilfps06f56aoskqn0
Theorem: Diaconescu-Goodman-Myhill Theorem

The {{Axiom-link|Choice}} implies the law of excluded middle.

Proof:
Let $\mathbb B = \set {0, 1}$. 
Let $p$ be a proposition.
Let the following two sets be defined:
:$A = \set {x \in \mathbb B: x = 0 \lor p}$
:$B = \set {x \in \mathbb B: x = 1 \lor p}$
where $\lor$ denotes the disjunction operator.
We have that:
:$0 \in A$
and:
:$1 \in B$
so both $A$ and $B$ are non-empty
Then the set:
:$X = \set {A, B}$
is a set of non-empty sets.
By the {{Axiom-link|Choice}}, there exists a choice function:
:$f: X \to \mathbb B$
since $\ds \bigcup X = \mathbb B$.
There are four cases:
:$(1): \quad \map f A = \map f B = 0$
This means that $0 \in B$.
But for that to happen, $\paren {0 = 1} \vee p$ must be true.
So by Disjunctive Syllogism, $p$ is true.
:$(2): \quad \map f A = \map f B = 1$
This means that $1 \in A$.
Arguing similarly to case $(1)$, it follows that  $p$ is true in this case also.
:$(3): \quad \map f A = 1 \ne \map f B = 0$
This means that $A \ne B$ (or otherwise $f$ would pick the same element).
But if $p$ is true, that means:
:$A = B = \mathbb B$
which is a contradiction.
Therefore in this case:
:$\neg p$
:$(4): \quad \map f A = 0 \ne \map f B = 1$
Using the same reasoning as in case $(3)$, it is seen that in this case:
:$\neg p$
So by Proof by Cases:
:$\paren {p \vee \neg p}$
That is the Law of Excluded Middle.
{{qed}}
{{Namedfor|Radu Diaconescu|name2 = Noah D. Goodman|name3 = John R. Myhill|cat = Diaconescu|cat2 = Goodman, N.D.|cat3 = Myhill}}
Theorem: Characterization of Boundary by Basis

Let $T = \struct {S, \tau}$ be a topological space.
Let $\BB \subseteq \tau$ be a basis.
Let $A$ be a subset of $T$.
Let $x$ be a point of $T$.
Then $x \in \partial A$ {{iff}}:
:for every $U \in \BB$:
::if $x \in U$
::then $A \cap U \ne \O$ and $\relcomp S A \cap U \ne \O$
where:
:$\relcomp S A = S \setminus A$ denotes the complement of $A$ in $S$
:$\partial A$ denotes the boundary of $A$ in $T$.

Proof:
=== Sufficient Condition ===
Let $x \in \partial A$.
Let $U \in \BB$.
By definition of basis, $U$ is an open set of $T$.
Thus from Characterization of Boundary by Open Sets:
:if $x \in U$
::then $A \cap U \ne \O$ and $\relcomp S A \cap U \ne \O$.
{{qed|lemma}}
Theorem: Union of Interiors and Boundary Equals Whole Space

Let $T = \struct {S, \tau}$ be a topological space.
Let $A$ be a subset of $T$.
Then:
:$S = \Int A \cup \partial A \cup \Int {A'}$
where:
:$A' = S \setminus A$ denotes the complement of $A$ relative to $S$
:$\Int A$ denotes the interior of $A$
:$\partial A$ denotes the boundary of $A$.

Proof:
{{begin-eqn}}
{{eqn | l = \Int A \cup \partial A \cup \Int {A'}
      | r = \Int A \cup \Int {A'} \cup \partial A
      | c = Union is Associative, Union is Commutative
}}
{{eqn | r = \Int A \cup \Int {A'} \cup \paren {\map \cl A \cap \map \cl {A'} }
      | c = Boundary is Intersection of Closure with Closure of Complement
}}
{{eqn | r = \paren {\Int A \cup \Int {A'} \cup \map \cl A} \cap \paren {\Int A \cup \Int {A'} \cup \map \cl {A'} }
      | c = Intersection Distributes over Union
}}
{{eqn | r = \paren {\Int A \cup \paren {\map \cl A}' \cup \map \cl A} \cap \paren {\Int A \cup \Int {A'} \cup \map \cl {A'} }
      | c = Complement of Interior equals Closure of Complement
}}
{{eqn | r = \paren {\Int A \cup \paren {\paren {\map \cl A}' \cup \map \cl A} } \cap \paren {\Int A \cup \Int {A'} \cup \map \cl {A'} }
      | c = Union is Associative
}}
{{eqn | r = \paren {\Int A \cup S} \cap \paren {\Int A \cup \Int {A'} \cup \map \cl {A'} }
      | c = Union with Relative Complement
}}
{{eqn | r = \paren {\Int A \cup S} \cap \paren {\Int A \cup \Int {A'} \cup \paren {\Int A}'}
      | c = Complement of Interior equals Closure of Complement
}}
{{eqn | r = \paren {\Int A \cup S} \cap \paren {\Int A \cup \paren {\Int A' \cup \Int {A'} } }
      | c = Union is Associative, Union is Commutative
}}
{{eqn | r = \paren {\Int A \cup S} \cap \paren {S \cup \Int {A'} }
      | c = Union with Relative Complement
}}
{{eqn | r = S \cap \paren {S \cup \Int {A'} }
      | c = Union with Superset is Superset
}}
{{eqn | r = S \cap S
      | c = Union with Superset is Superset
}}
{{eqn | r = S
      | c = Set Intersection is Idempotent
}}
{{end-eqn}}
{{qed}}
Theorem: Characterization of Derivative by Open Sets

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'$
{{iff}}:
: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$
{{qed|lemma}}
Theorem: Characterization of Derivative by Local Basis

Let $T = \struct {S, \tau}$ be a topological space.
Let $A$ be a subset of $S$.
Let $x$ be a point of $T$.
Let $\BB \subseteq \tau$ be a local basis at $x$.
Then
:$x \in A'$
{{iff}}:
:for every $U \in \BB$, 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'$.
By Characterization of Derivative by Open Sets:
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$
As the elements of $\BB$ are all open sets, it follows that:
For every open set $U \in \BB$:
:if $x \in U$
:then there exists a point $y$ of $T$ such that $y \in A \cap U$ and $x \ne y$
{{qed|lemma}}
Theorem: Derivative is Included in Closure

Let $T = \struct {S, \tau}$ 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 \O$.
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 \O$
Hence the result.
{{qed}}
Theorem: Closure Equals Union with Derivative

Let $T = \struct {S, \tau}$ be a topological space.
Let $A$ be a subset of $S$.
Then:
:$A^- = A \cup A'$
where
:$A'$ denotes the derivative of $A$
:$A^-$ denotes the closure of $A$.

Proof:
=== Closure Subset of Union ===
It is to be proved that:
:$A^- \subseteq A \cup A'$
Let $x \in A^-$.
In the case where $x \in A$ then $x \in A \cup A'$ by definition of set union.
Let:
:$(1): \quad x \notin A$
From Characterization of Derivative by Open Sets, to prove $x \in A'$ it is enough to show that:
: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$.
Let $U$ be an open set of $T$.
Let $x \in U$.
Then by Condition for Point being in Closure:
:$A \cap U \ne \O$
Then by definition of empty set:
:$\exists y \in S: y \in A \cap U$
By definition of set intersection:
:$y \in A$ and $y \in U$
But as $x \notin A$ it follows by definition of set intersection that:
:$x \notin A \cap U$
So by $(1)$:
:$x \ne y$
Thus $y$ fulfils the conditions of the hypothesis, and so:
:$x \in A'$
Hence by definition of set union:
:$x \in A \cup A'$
Thus in all cases:
:$x \in A^- \implies x \in A \cup A'$
and so:
:$A^- \subseteq A \cup A'$
{{qed|lemma}}
Theorem: Derivative of Subset is Subset of Derivative

Let $T = \struct {S, \tau}$ be a topological space.
Let $A$, $B$ be subsets of $S$.
Then
:$A \subseteq B \implies A' \subseteq B'$
where $A'$ denotes the derivative of $A$ in $T$.

Proof:
Let $A \subseteq B$.
Let $x \in A'$.
By Characterization of Derivative by Open Sets it is enough to prove that:
:for every open set $G$ of $T$:
::if $x \in G$
::then there exists $y$ such that $y \in B \cap G$ and $x \ne y$.
Let $G$ be an open set of $T$.
Let $x \in G$.
Then by Characterization of Derivative by Open Sets:
:there exists a point $y$ of $T$ such that $y \in A \cap G$ and $x \ne y$.
By {{Corollary|Set Intersection Preserves Subsets}}:
:$A \cap G \subseteq B \cap G$
Hence:
:$y \in B \cap G$ and $x \ne y$.
The conditions of the hypothesis are thus fulfilled, and:
:$x \in B'$
Thus by definition of subset:
:$A' \subseteq B'$
{{qed}}
Theorem: Derivative of Union is Union of Derivatives

Let $T = \struct {S, \tau}$ be a topological space.
Let $A$, $B$ be subsets of $S$.
Then
:$\paren {A \cup B}' = A' \cup B\,'$
where
:$A'$ denotes the derivative of $A$.

Proof:
=== Derivative of Union subset of Union of Derivatives ===
It will be shown that:
:$\paren {A \cup B}' \subseteq A' \cup B\,'$
Let $x \in \paren {A \cup B}'$.
By definition of set derivative:
:$x$ is an accumulation point of $A \cup B$.
Then by definition of accumulation point of set:
:$(1): \quad x \in \paren {\paren {A \cup B} \setminus \set x}^-$
where $A^-$ denotes the closure of $A$.
By Set Difference is Right Distributive over Union:
:$\paren {A \cup B} \setminus \set x = \paren {A \setminus \set x} \cup \paren {B \setminus \set x}$
Then by Closure of Finite Union equals Union of Closures:
:$\paren {\paren {A \cup B} \setminus \set x}^- = \paren {A \setminus \set x}^- \cup \paren {B \setminus \set x}^-$
Then by $(1)$ and definition of set union:
:$x \in \paren {A \setminus \set x}^-$ or $x \in \paren {B \setminus \set x}^-$
Then by definition of accumulation point of set:
:$x$ is an accumulation point of $A$ or $x$ is an accumulation point of $B$.
Then by definition of set derivative:
:$x \in A'$ or $x \in B\,'$
Hence by definition of set union:
:$x \in A' \cup B\,'$
Theorem: Derivative of Derivative is Subset of Derivative in T1 Space

Let $T = \struct {S, \tau}$ 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' '$
{{AimForCont}} $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:
:$\set x$ is closed.
Then by Open Set minus Closed Set is Open:
:$(4): \quad G \setminus \set 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 \set x$
By definition of intersection and $(5)$:
:$y \in G$
By $(6)$ and definition of singleton:
:$y \notin \set x$
Then by definition of set difference:
:$(8): \quad y \in G \setminus \set x$
We will prove:
:$(9): \quad G \cap \paren {A \setminus \set x} = \O$
:{{AimForCont}}:
:: $G \cap \paren {A \setminus \set x} \ne \O$
:Then by definition of the empty set there exists $g$ such that:
::$g \in G \cap \paren {A \setminus \set x}$
:Hence by definition of intersection:
:: $g \in G$
:and:
:: $g \in A \setminus \set x$
:Then by definition of set difference:
::$g \in A$ 
:Hence by definition of intersection:
:: $g \in A \cap G$
:Then by $(3)$:
:: $x = g$
:This by definition of singleton contradicts with $g \notin \set x$ obtained by definition of set difference.
:Thus:
::$G \cap \paren {A \setminus \set x} = \O$
Define $U = G \setminus \set 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 \set y$
Then by definition of set difference
:$(12): \quad q \in A \setminus \set y$
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 \set x$
and :
:$q \in G$
Hence this contradicts with $(9)$ by definition of intersection.
Thus the result by Proof by Contradiction.
{{qed}}
Theorem: Closure of Derivative is Derivative in T1 Space

Let $T = \struct {S, \tau}$ be a $T_1$ topological space.
Let $A$ be a subset of $S$.
Then
:$A'^- = A'$
where
:$A'$ denotes the derivative of $A$
:$A^-$ denotes the closure of $A$.

Proof:
{{begin-eqn}}
{{eqn | l = A'^-
      | r = A' \cup A' '
      | c = Closure Equals Union with Derivative
}}
{{eqn | o = \subseteq
      | r = A' \cup A'
      | c = $A' ' \subseteq A'$ by Derivative of Derivative is Subset of Derivative in T1 Space
}}
{{eqn | r = A'
      | c = Set Union is Idempotent
}}
{{end-eqn}}
So:
:$A'^- \subseteq A'$
Then by  definition of closure:
:$A' \subseteq A'^-$
Hence the result by definition of set equality.
{{qed}}
Theorem: Union of Derivatives is Subset of Derivative of Union

Let $T = \struct {S, \tau}$ be a topological space.
Let:
:$\FF \subseteq \powerset S$ be a set of subsets of $S$
where $\powerset S$ denotes the power set of $S$.
Then:
:$\ds \bigcup_{A \mathop \in \FF} A' \subseteq \paren {\bigcup_{A \mathop \in \FF} A}'$
where $A'$ denotes the derivative of $A$.

Proof:
Let $\ds x \in \bigcup_{A \mathop \in \FF} A'$.
Then by definition of union there exists $A \in \FF$ such that:
:$(1): \quad x \in A'$
By Set is Subset of Union:
:$\ds A \subseteq \bigcup_{A \mathop \in \FF} A$
Then by Derivative of Subset is Subset of Derivative:
:$\ds A' \subseteq \paren {\bigcup_{A \mathop \in \FF} A}'$
Hence by $(1)$ the result:
:$\ds x \in \paren {\bigcup_{A \mathop \in \FF} A}'$
follows by definition of subset.
{{qed}}
Theorem: Point is Isolated iff not Accumulation Point

Let $T = \struct {S, \tau}$ be a topological space.
Let $H \subseteq S$.
Let $x \in H$.
Then:
:$x$ is an isolated point in $H$
{{iff}}:
:$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 = \set x$
That is, by definition of uniqueness:
:$\lnot \forall U \in \tau: \paren {x \in U \implies \exists y \in S: \paren {y \in H \cap U \land x \ne y} }$
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$.
{{qed|lemma}}
Theorem: Point is Isolated iff belongs to Set less Derivative

Let $T = \left({S, \tau}\right)$ be a topological space.
Let $H \subseteq S$.
Let $x \in S$.
Then:
:$x$ is an isolated point in $H$
{{iff}}:
:$x \in H \setminus H'$
where
:$H'$ denotes the derivative of $H$.

Proof:
$x$ is an isolated point in $H$
$\iff$ $x \in H$ and $x$ is not an accumulation point of $H$ by Point is Isolated iff not Accumulation Point
$\iff$ $x \in H$ and $x \notin H'$ by definition of derivative
$\iff$ $x \in H \setminus H'$ by definition of set difference.
{{qed}}
Theorem: Dense-in-itself iff Subset of Derivative

Let $T$ be a topological space.
Let $A \subseteq T$.
Then:
:$A$ is dense-in-itself
{{iff}}:
:$A \subseteq A'$
where $A'$ denotes the derivative of $A$.

Proof:
{{begin-eqn}}
{{eqn | o =
      | c = $A$ is dense-in-itself
}}
{{eqn | ll= \leadstoandfrom
      | o =
      | c = every $x \in A$ is not an isolated point in $A$
      | cc= {{Defof|Dense-in-itself}}
}}
{{eqn | ll= \leadstoandfrom
      | o =
      | c = every $x \in A$ is an accumulation point of $A$
      | cc= Point is Isolated iff not Accumulation Point
}}
{{eqn | ll= \leadstoandfrom
      | o =
      | c = every $x \in A$ is an element of $A'$
      | cc= {{Defof|Set Derivative}}
}}
{{eqn | ll= \leadstoandfrom
      | o =
      | c = $A \subseteq A'$
      | cc= {{Defof|Subset}}
}}
{{end-eqn}}
{{qed}}
Category:Set Derivatives
Category:Dense-in-itself
3l31htxahytgg17dyepnhuuhhb7de0f
Theorem: Closure of Dense-in-itself is Dense-in-itself in T1 Space

Let $T$ be a $T_1$ topological space.
Let $A \subseteq T$. 
Let $A$ be dense-in-itself.
Then the closure $A^-$ of $A$ is also dense-in-itself.

Proof:
Let $A$ be dense-in-itself.
Then by Dense-in-itself iff Subset of Derivative:
:$(1): \quad A \subseteq A'$
where $A'$ denotes the derivative of $A$.
By Derivative of Derivative is Subset of Derivative in $T_1$ Space:
:$(2): \quad A' ' \subseteq A'$
By Dense-in-itself iff Subset of Derivative it is sufficient to proof that:
:$A^- \subseteq \paren {A^-}'$
Thus:
{{begin-eqn}}
{{eqn | l = \paren {A^-}'
      | r = \paren {A \cup A'}'
      | c = Closure Equals Union with Derivative
}}
{{eqn | r = A' \cup A' '
      | c = Derivative of Union is Union of Derivatives
}}
{{eqn | r = A'
      | c = $(2)$ and Union with Superset is Superset
}}
{{eqn | r = A \cup A'
      | c = $(1)$ and Union with Superset is Superset
}}
{{eqn | r = A^-
      | c = Closure Equals Union with Derivative
}}
{{end-eqn}}
{{qed}}
Theorem: Union of Set of Dense-in-itself Sets is Dense-in-itself

Let $T$ be a topological space.
Let $\FF \subseteq \powerset T$ such that:
:every element of $\FF$ is dense-in-itself.
Then the union $\bigcup \FF$ is also dense-in-itself.

Proof:
By Dense-in-itself iff Subset of Derivative:
:$\forall A \in \FF: A \subseteq A'$
where $A'$ denotes the derivative of $A$.
Then by Set Union Preserves Subsets:
:$\ds \bigcup \FF \subseteq \bigcup_{A \mathop \in \FF} A'$
By Union of Derivatives is Subset of Derivative of Union:
:$\ds \bigcup_{A \mathop \in \FF} A' \subseteq \paren {\bigcup \FF}'$
Then by Subset Relation is Transitive:
:$\ds \bigcup \FF \subseteq \paren {\bigcup \FF}'$
The result follows by Dense-in-itself iff Subset of Derivative.
{{qed}}
Theorem: Equivalence of Definitions of Weight of Topological Space

Let $T$ be a topological space.
Let $\mathbb B$ be the set of all bases of $T$.
The following definitions of the weight of $T$ are equivalent:
=== Definition 1 ===
{{:Definition:Weight of Topological Space/Definition 1}}
=== Definition 2 ===
{{:Definition:Weight of Topological Space/Definition 2}}

Proof:
By Class of All Cardinals is Subclass of Class of All Ordinals, the set:
:$M = \set {\card \BB: \BB \in \mathbb B}$
is a subclass of the class of all ordinals.
By Class of All Ordinals is Well-Ordered by Subset Relation:
:$M$ is well ordered by the $\subseteq$ relation.
By Class of All Ordinals is Well-Ordered by Subset Relation there exists a smallest element $m_0 \in M$:
:$\forall m \in M: m_0 \subseteq m$
Hence by Smallest Element is Minimal there exists a basis $\BB_0$ of $T$ which has minimal cardinality:
:$m_0 = \map {w_2} T$.
Let:
:$\ds \map {w_1} T = \bigcap_{\BB \mathop \in \mathbb B} \card \BB$
By Intersection is Subset:
:$\ds \map {w_1} T = \bigcap M \subseteq m_0$
But by Intersection is Largest Subset:
:$\ds \mathfrak m_0 \subseteq \bigcap M$
By definition of set equality:
:$\map {w_1} T = \map {w_2} T$
and hence the result.
{{qed}}
Theorem: Space is First-Countable iff Character not greater than Aleph 0

Let $T$ be a topological space.
$T$ is first-countable {{iff}}:
:$\map \chi T \le \aleph_0$
where $\map \chi T$ denotes the character of $T$.

Proof:
=== Sufficient Condition ===
Let $T$ be first-countable.
By definition of first-countable:
:$\forall x \in T: \exists \BB \in \map {\mathbb B} x: \card \BB \le \aleph_0$
where $\map {\mathbb B} x$ denotes the set of all local bases at $x$.
Then by definition of character of a point:
:$\forall x \in T: \map \chi {x, T} \le \aleph_0$
Hence by definition of character of topogical space:
:$\map \chi T \le \aleph_0$
{{qed|lemma}}
Theorem: Difference of Two Powers/Examples/Difference of Two Cubes

:$x^3 - y^3 = \paren {x - y} \paren {x^2 + x y + y^2}$

Proof:
From Difference of Two Powers:
:$\ds a^n - b^n = \paren {a - b} \sum_{j \mathop = 0}^{n - 1} a^{n - j - 1} b^j$
The result follows directly by setting $n = 3$.
{{qed}}