avewright/proofwiki-math huggingface dataset:
Theorem: Field Generated by Macroscopic Charge Density

Let $B$ be a body of matter.
Let $P$ be a point inside $B$ whose position vector is $\mathbf r$.
The electric field at $P$ generated by the macroscopic charge density within $B$ is given by:
:$\ds \map {\mathbf E} {\mathbf r} = \dfrac 1 {4 \pi \varepsilon_0} \int_{\text {all space} } \dfrac {\paren {\mathbf r - \mathbf r'} \map \rho {\mathbf r'} } {\size {\mathbf r - \mathbf r'}^3} \rd V'$
where:
:$\d V'$ is an infinitesimal volume element
:$\mathbf r'$ is the position vector of $\d V'$
:$\map \rho {\mathbf r'}$ is the macroscopic charge density of the macroscopic electric field at $\mathbf r'$
:$\varepsilon_0$ denotes the vacuum permittivity.

Proof:
From Electric Field Strength from Assemblage of Point Charges, the electric field strength caused by an assemblage of point charges $q_1, q_2, \ldots, q_n$ is given by:
:$\ds \map {\mathbf E} {\mathbf r} = \dfrac 1 {4 \pi \epsilon_0} \sum_i \dfrac {\paren {\mathbf r - \mathbf r_i} q_i} {\size {\mathbf r - \mathbf r_i}^3}$
where $\mathbf r_1, \mathbf r_2, \ldots, \mathbf r_n$ are the position vectors of $q_1, q_2, \ldots, q_n$ respectively.
We apply the same principle to the macroscopic charge density and convert the summation into a definite integral, as follows:
Consider a volume element $\d V'$ which is smaller than the scale used for a macroscopic electric field, but still large enough to contain many atoms.
:400px
The electric field strength caused by $\d V'$ is:
:$\map {\mathbf E_{\text {atomic} } } {\mathbf r'} = \dfrac 1 {4 \pi \epsilon_0} \dfrac {\paren {\mathbf r - \mathbf r'} \rd q} {\size {\mathbf r - \mathbf r'}^3}$
where $\d q$ is the electric charge on $\d V'$.
By definition of macroscopic charge density:
:$\map \rho {\mathbf r'} = \dfrac {\d q} {\d V'}$
and so:
:$\map {\mathbf E} {\mathbf r'} = \dfrac 1 {4 \pi \epsilon_0} \dfrac {\paren {\mathbf r - \mathbf r'} \map \rho {\mathbf r'} } {\size {\mathbf r - \mathbf r'}^3} \rd V'$
Integrating over all space:
:$\ds \map {\mathbf E} {\mathbf r} = \dfrac 1 {4 \pi \varepsilon_0} \int_{\text {all space} } \dfrac {\paren {\mathbf r - \mathbf r'} \map \rho {\mathbf r'} } {\size {\mathbf r - \mathbf r'}^3} \rd V'$
Hence the result.
{{qed}}
Theorem: Field Generated by Surface Charge Density

Let $B$ be a body of matter.
Let $P$ be a point inside $B$ whose position vector is $\mathbf r$.
The electric field at $P$ generated by the surface charge density over $B$ is given by:
:$\ds \map {\mathbf E} {\mathbf r} = \dfrac 1 {4 \pi \varepsilon_0} \int_{\text {all surfaces} } \dfrac {\paren {\mathbf r - \mathbf r'} \map \sigma {\mathbf r'} } {\size {\mathbf r - \mathbf r'}^3} \rd S'$
where:
:$\d S'$ is an infinitesimal area element
:$\mathbf r'$ is the position vector of $\d S'$
:$\map \sigma {\mathbf r'}$ is the surface charge density at $\mathbf r'$
:$\varepsilon_0$ denotes the vacuum permittivity.

Proof:
From Electric Field Strength from Assemblage of Point Charges, the electric field strength caused by an assemblage of point charges $q_1, q_2, \ldots, q_n$ is given by:
:$\ds \map {\mathbf E} {\mathbf r} = \dfrac 1 {4 \pi \epsilon_0} \sum_i \dfrac {\paren {\mathbf r - \mathbf r_i} q_i} {\size {\mathbf r - \mathbf r_i}^3}$
where $\mathbf r_1, \mathbf r_2, \ldots, \mathbf r_n$ are the position vectors of $q_1, q_2, \ldots, q_n$ respectively.
We apply the same principle to the surface charge density and convert the summation into a definite integral, as follows:
Consider an area element $\d S'$.
The electric field strength caused by $\d S'$ is:
:$\map {\mathbf E} {\mathbf r'} = \dfrac 1 {4 \pi \epsilon_0} \dfrac {\paren {\mathbf r - \mathbf r'} \rd q} {\size {\mathbf r - \mathbf r'}^3}$
where $\d q$ is the electric charge on $\d S'$.
By definition of surface charge density:
:$\map \sigma {\mathbf r'} = \dfrac {\d q} {\d S'}$
and so:
:$\map {\mathbf E} {\mathbf r'} = \dfrac 1 {4 \pi \epsilon_0} \dfrac {\paren {\mathbf r - \mathbf r'} \map \sigma {\mathbf r'} } {\size {\mathbf r - \mathbf r'}^3} \rd S'$
Integrating over all surfaces of $B$:
:$\ds \map {\mathbf E} {\mathbf r} = \dfrac 1 {4 \pi \varepsilon_0} \int_{\text {all surfaces} } \dfrac {\paren {\mathbf r - \mathbf r'} \map \rho {\mathbf r'} } {\size {\mathbf r - \mathbf r'}^3} \rd S'$
Hence the result.
{{qed}}
Theorem: Macroscopic Electric Field in Body

Let $B$ be a body of matter.
Let $P$ be a point inside $B$ whose position vector is $\mathbf r$.
The macroscopic electric field at $P$ is given by:
:$\ds \map {\mathbf E} {\mathbf r} = \dfrac 1 {4 \pi \varepsilon_0} \int_{\text {all space} } \dfrac {\paren {\mathbf r - \mathbf r'} \map \rho {\mathbf r'} } {\size {\mathbf r - \mathbf r'}^3} \rd V' + \dfrac 1 {4 \pi \varepsilon_0} \int_{\text {all surfaces} } \dfrac {\paren {\mathbf r - \mathbf r'} \map \sigma {\mathbf r'} } {\size {\mathbf r - \mathbf r'}^3} \rd S'$
where:
:$\d V'$ is an infinitesimal volume element
:$\d S'$ is an infinitesimal area element
:$\mathbf r'$ is the position vector of $\d V'$ or $\d S'$ as appropriate
:$\map \rho {\mathbf r'}$ is the macroscopic charge density of the macroscopic electric field at $\mathbf r'$
:$\varepsilon_0$ denotes the vacuum permittivity.

Proof:
From Field Generated by Macroscopic Charge Density, the electric field at $P$ generated by the macroscopic charge density within $B$ is given by:
:$\ds \map {\mathbf E} {\mathbf r} = \dfrac 1 {4 \pi \varepsilon_0} \int_{\text {all space} } \dfrac {\paren {\mathbf r - \mathbf r'} \map \rho {\mathbf r'} } {\size {\mathbf r - \mathbf r'}^3} \rd V'$
From Field Generated by Surface Charge Density, the electric field at $P$ generated by the surface charge density over $B$ is given by:
:$\ds \map {\mathbf E} {\mathbf r} = \dfrac 1 {4 \pi \varepsilon_0} \int_{\text {all surfaces} } \dfrac {\paren {\mathbf r - \mathbf r'} \map \sigma {\mathbf r'} } {\size {\mathbf r - \mathbf r'}^3} \rd S'$
We have that the Electric Field satisfies Principle of Superposition.
Hence the total macroscopic electric field at $P$ is given by the sum of these:
:$\ds \map {\mathbf E} {\mathbf r} = \dfrac 1 {4 \pi \varepsilon_0} \int_{\text {all space} } \dfrac {\paren {\mathbf r - \mathbf r'} \map \rho {\mathbf r'} } {\size {\mathbf r - \mathbf r'}^3} \rd V' + \dfrac 1 {4 \pi \varepsilon_0} \int_{\text {all surfaces} } \dfrac {\paren {\mathbf r - \mathbf r'} \map \sigma {\mathbf r'} } {\size {\mathbf r - \mathbf r'}^3} \rd S'$
{{qed}}
Theorem: Characterization of Open Set by Open Cover

Let $T = \struct{S, \tau}$ be a topological space.
Let $\UU$ be an open cover of $T$.
For each $U \in \UU$, let $\tau_U$ denote the subspace topology on $U$.
Let $W \subseteq S$.
Then $W$ is open in $T$ {{iff}}:
:$\forall U \in \UU: W \cap U$ is open in $\struct{U, \tau_U}$

Proof:
=== Necessary Condition ===
This follows immediately from the definition of subspace topology.
{{qed|lemma}}
Theorem: Characterization of Closed Set by Open Cover

Let $T = \struct{S, \tau}$ be a topological space.
Let $\UU$ be an open cover of $T$.
For each $U \in \UU$, let $\tau_U$ denote the subspace topology on $U$.
Let $F \subseteq S$.
Then $F$ is closed in $T$ {{iff}}:
:$\forall U \in \UU: F \cap U$ is closed in $\struct{U, \tau_U}$

Proof:
=== Necessary Condition ===
This follows immediately from Closed Set in Topological Subspace.
{{qed|lemma}}
Theorem: Union of Closed Locally Finite Set of Subsets is Closed

Let $T = \struct{S, \tau}$ be a topological space.
Let $\FF$ be a closed locally finite set of subsets of $T$.
Let $E = \ds \bigcup \FF$.
Then:
:$E$ is closed in $T$.

Proof:
Let:
:$\UU = \leftset {U \in \tau : \set {F \in \FF : U \cap F \ne \O}}$ is finite $\rightset{}$
By definition of closed locally finite set of subsets:
:$\forall x \in S : \exists U \in \tau : x \in U : \set{F \in \FF : U \cap F \ne \O}$ is finite
That is:
:$\forall x \in S : \exists U \in \UU : x \in U$
Hence
:$\UU$ is a open cover of $T$ by definition.
Let $U \in \UU$.
Let $\FF_U = \set {F \in \FF : F \cap U \ne \O}$ 
We have:
{{begin-eqn}}
{{eqn | l = U \cap E
      | r = U \cap \paren {\cup \set{F : F \in \FF} }
}}
{{eqn | r = \cup \set {U \cap F : F \in \FF}
      | c = Intersection Distributes over Union
}}
{{eqn | r = \cup \set {U \cap F : F \in \FF_U}
      | c = Union with Empty Set
}}
{{end-eqn}}
From Closed Set in Topological Subspace:
:$\forall F \in \FF_U : U \cap F$ is closed in the subspace topology on $U$
From {{:Template:Closed-set-axiom|2}}:
:$U \cap E$ is closed in the subspace topology on $U$
Since $U$ was an arbitrary element of $\UU$:
:$\forall U \in \UU : U \cap E$ is closed in the subspace topology on $U$
From Characterization of Closed Set by Open Cover:
:$E$ is closed in $T$ 
{{qed}}
Category:Locally Finite Sets of Subsets
5x9r9cybohtu6z9av7lrllheveiqc37
Theorem: Closures of Elements of Locally Finite Set is Locally Finite

Let $T = \struct{S, \tau}$ be a topological space.
Let $\AA$ be a locally finite set of subsets of $T$.
Then:
:$\set{A^- : A \in \AA}$ is locally finite in $T$
where $A^-$ denotes the closure of $A$ in $T$.

Proof:
Let $\BB = \set{A^- : A \in \AA}$.
Let $x \in S$.
By definition of locally finite set of subsets:
:$\exists U_x \in \tau : x \in U_x :$ the set $\AA_x = \set{A \in \AA : A \cap U_x \ne \O}$ is finite
Let $\BB_x = \set{A^- \in \BB : A^- \cap U_x \ne \O}$
Let $A^- \in \BB_x$.
From Open Set Disjoint from Set is Disjoint from Closure:
:$U_x \cap A \ne \O$
Hence:
:$A \in \AA_x$
It follows that $\BB_x$ is finite.
Since $x$ was arbitrary, we have shown that:
:$\forall x \in S : \exists U_x \in \tau : x \in U_x :$ the set $\BB_x = \set{A^- \in \BB : A^- \cap U_x \ne \O}$ is finite
Hence $\BB$ is locally finite set of subsets by definition.
{{qed}}
Category:Locally Finite Sets of Subsets
n6a5oynemslc8hwibgnxv8zzu8juog9
Theorem: Union of Closures of Elements of Locally Finite Set is Closed

Let $T = \struct{S, \tau}$ be a topological space.
Let $\AA$ be a locally finite set of subsets of $T$.
Then:
:$\ds \paren {\bigcup \AA}^- = \bigcup \set{A^- : A \in \AA}$
where $A^-$ denotes the closure of $A$ in $T$.

Proof:
From Closures of Elements of Locally Finite Set is Locally Finite:
:$\set{A^- : A \in \AA}$ is also locally finite
From Union of Closed Locally Finite Set of Subsets is Closed:
:$\bigcup \set{A^- : A \in \AA}$ is closed in $T$
We have:
{{begin-eqn}}
{{eqn | q = \forall A \in \AA
      | l = A
      | o = \subseteq
      | r = A^-
      | c = Set is Subset of its Topological Closure
}}
{{eqn | r = \bigcup \set{A^- : A \in \AA}
      | c = Set is Subset of Union
}}
{{eqn | ll = \leadsto
      | l = \bigcup \AA
      | o = \subseteq
      | r = \bigcup \set{A^- : A \in \AA}
      | c = Union of Subsets is Subset
}}
{{eqn | ll = \leadsto
      | l = \paren{\bigcup \AA}^-
      | o = \subseteq
      | r = \bigcup \set{A^- : A \in \AA}
      | c = Closure of Subset of Closed Set of Topological Space is Subset
}}
{{end-eqn}}
From Closure of Union contains Union of Closures
:$\ds \bigcup \set{A^- : A \in \AA} \subseteq \paren {\bigcup \AA}^-$
By definition of set equality:
:$\ds \paren {\bigcup \AA}^- = \bigcup \set{A^- : A \in \AA}$
{{qed}}
Category:Locally Finite Sets of Subsets
4xanj631tz1573ycfsmcgc8bogtfitr
Theorem: Electric Flux out of Closed Surface surrounding Point Charge

Let $q$ be a point charge.
Let $S$ be a closed surface surrounding $q$.
The total electric flux through $S$ is given by:
:$F = \dfrac q {\varepsilon_0}$

Proof:
=== Lemma ===
{{:Electric Flux out of Closed Surface surrounding Point Charge/Lemma}}{{qed|lemma}}
From this lemma, we can transform the surface integral for the flux through the entire surface $S$ into a double integral between angles:
{{begin-eqn}}
{{eqn | l = \int_S \mathbf E \cdot \rd \mathbf S
      | r = \dfrac q {4 \pi \varepsilon_0} \int_0^\pi \sin \theta \rd \theta \int_0^{2 \pi} \rd \phi
      | c = 
}}
{{eqn | r = \dfrac q {4 \pi \varepsilon_0} \int_0^\pi \sin \theta \rd \theta \bigintlimits \phi 0 {2 \pi}
      | c = 
}}
{{eqn | r = \dfrac q {4 \pi \varepsilon_0} \int_0^\pi \sin \theta \rd \theta \times 2 \pi
      | c = 
}}
{{eqn | r = \dfrac q {2 \varepsilon_0} \int_0^\pi \sin \theta \rd \theta
      | c = 
}}
{{eqn | r = \dfrac q {2 \varepsilon_0} \bigintlimits {-\cos \theta} 0 \pi
      | c = 
}}
{{eqn | r = \dfrac q {2 \varepsilon_0} \paren {-\paren {\cos \pi - \cos 0} }
      | c = 
}}
{{eqn | r = \dfrac q {2 \varepsilon_0} \paren {-\paren {-1 - 1} }
      | c = 
}}
{{eqn | r = \dfrac q {\varepsilon_0}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Electric Flux out of Closed Surface surrounding Point Charge/Lemma

Let $q$ be a point charge located at the origin of a spherical polar coordinate system.
{{DefinitionWanted|Spherical Polar Coordinate System}}
Let $S$ be a closed surface surrounding $q$.
Let $\delta \mathbf S$ be an area element of $S$.
Let $\delta \Omega$ be the solid angle subtended by the projection of $\delta \mathbf S$ from $q$.
The total electric flux through $\delta \Omega$ is given by:
:$F = \dfrac q {4 \pi \varepsilon_0} \delta \Omega$

Proof:
Consider the area element $\delta \mathbf S$ at the position $P$ with position vector $\mathbf r$ whose spherical coordinates are $\polar {r, \theta, \phi}$.
Let $\delta S_p$ be the projected area of $\delta \mathbf S$ to the plane perpendicular to $\mathbf r$.
:500px
Let us define $\delta \mathbf S$ as being the subset of the surface of $S$ demarcated by the arcs on $S$ subtending:
:the polar angles $\theta$ and $\delta \theta$ and 
and:
:the azimuthal angles $\phi$ and $\delta \phi$.
From the above diagram:
:$\delta S_p = r^2 \sin \theta \rdelta \theta \rdelta \phi$
Let $\mathbf E$ be the electric field generated by $q$ at $P$.
According to Coulomb's Law of Electrostatics:
:the magnitude of $\mathbf E$ is:
::$E = \dfrac q {4 \pi \varepsilon_0 r^2}$
:the direction of $\mathbf E$ is along $\mathbf r$ away from the origin.
Hence the electric flux in the direction away from the origin through $\delta \mathbf S$ is:
{{begin-eqn}}
{{eqn | l = \mathbf E \cdot \delta \mathbf S
      | r = E \rdelta S_p
      | c = 
}}
{{eqn | r = \dfrac q {4 \pi \varepsilon_0 r^2} r^2 \sin \theta \rdelta \theta \rdelta \phi
      | c = 
}}
{{eqn | r = \dfrac q {4 \pi \varepsilon_0} \sin \theta \rdelta \theta \rdelta \phi
      | c = 
}}
{{eqn | r = \dfrac q {4 \pi \varepsilon_0} \rdelta \Omega
      | c = 
}}
{{end-eqn}}
where $\Omega$ is that solid angle so subtended.
{{qed}}
Theorem: Electric Flux out of Closed Surface surrounding Assemblage of Point Charges

Let $Q = \set {q_1, q_2, \ldots}$ be a set of point charges.
Let $S$ be a closed surface surrounding $Q$.
The total electric flux through $S$ is given by:
:$\ds F = \dfrac 1 {\varepsilon_0} \sum_Q q_i$

Proof:
From Electric Flux out of Closed Surface surrounding Point Charge:
:$F_i = \dfrac {q_i} {\varepsilon_0}$
where $F_i$ is the part of $F$ brought about by $q_i$.
The result follows from Electric Field satisfies Principle of Superposition.
{{qed}}
Theorem: Electric Flux out of Closed Surface surrounding Body with Continuous Charge Distribution

Let $B$ be a body of matter which has a continuous macroscopic charge density $\map \rho {\mathbf r}$.
Let $S$ be a closed surface surrounding $Q$.
The total electric flux through $S$ generated by the electric charge on $B$ is given by:
:$\ds F = \dfrac 1 {\varepsilon_0} \int_V \map \rho {\mathbf r} \rd \tau$
where:
:$V$ is the total volume enclosed by $S$
:$\d \tau$ is an infinitesimal volume element
:$\mathbf r$ is the position vector of $\d \tau$
:$\map \rho {\mathbf r}$ is the macroscopic charge density of the macroscopic electric field at $\mathbf r$
:$\varepsilon_0$ denotes the vacuum permittivity.

Proof:
Let $\d \tau$ be an arbitrary infinitesimal volume element.
$\d \tau$ can be considered as an infinitesimal point charge $\d q$.
From Electric Flux out of Closed Surface surrounding Point Charge:
:$\d F_\tau = \dfrac {\d q} {\varepsilon_0}$
where $\d F_\tau$ is the infinitesimal part of $F$ brought about by $\d q$. 
By definition of macroscopic charge density:
:$\map \rho {\mathbf r} = \dfrac {\d q} {\d \tau}$
Hence:
:$\d F_\tau = \dfrac {\map \rho {\mathbf r} \rd \tau} {\varepsilon_0}$
Integrating over all space:
:$\ds F = \dfrac 1 {\varepsilon_0} \int_V \map \rho {\mathbf r} \rd \tau$
{{qed}}
Theorem: Rotation of Cartesian Axes around Vector

Let $\mathbf r$ be a vector in space.
Let a Cartesian plane $\CC$ be established such that:
:the initial point of $\mathbf r$ is at the origin $O$
:the terminal point of $\mathbf r$ is the point $P$.
Let $\tuple {X, Y}$ be the coordinates of $P$ under $\CC$.
Let $\CC$ be rotated about $O$ to $\CC'$, through an angle $\varphi$ in the anticlockwise direction, while keeping $\mathbf r$ fixed.
Let $\tuple {X', Y'}$ be the coordinates of $P$ under $\CC'$.
Then:
{{begin-eqn}}
{{eqn | l = X'
      | r = X \cos \varphi + Y \sin \varphi
}}
{{eqn | l = Y'
      | r = -X \sin \varphi + Y \cos \varphi
}}
{{end-eqn}}

Proof:
:500px
With reference to the above diagram:
:$X P X' = \varphi$
and so:
:$OX' = OX \cos \varphi + PX \sin \varphi$
and:
:$OY' = OY \cos \varphi - PY \cos \varphi$
Hence the result.
{{qed}}
Theorem: Hex Theorem

A Hex board in which every tile is marked has exactly one winner.

Proof:
{{ProofWanted}}
Category:Hex Theorem
Category:Hex (Game)
mqwpdq7b61fgqddeqg26n5q0l8p9vmx
Theorem: T3 Space with Sigma-Locally Finite Basis is T4 Space/Lemma 1

Let $F$ be a closed subset of $T$.
Let $X \subseteq S$ be disjoint from $F$.
Then there exists a countable open cover $\WW = \set{W_n : n \in \N}$ of $X$:
:$\forall n \in \N : W_n^- \cap F = \O$

Proof:
Let $\UU = \set {U \in \BB : U^- \cap F = \O}$.
Theorem: T3 Space with Sigma-Locally Finite Basis is T4 Space/Lemma 2

Let $x \in S \setminus F$.
Then:
:$\exists U \in \BB : x \in U : U^- \cap F = \O$

Proof:
From Characterization of T3 Space:
:$\exists W \in \tau: x \in W : W^- \cap F = \O$
By definition of basis:
:$\exists U \in \BB : x \in U \subseteq W$
From Topological Closure of Subset is Subset of Topological Closure:
:$U^- \subseteq W^-$
From Set Intersection Preserves Subsets:
:$U^- \cap F = \O$
{{qed}}
Category:T3 Space with Sigma-Locally Finite Basis is T4 Space
cnpmcyj9mk7bofvx8qm1n3jkbn0x5fj
Theorem: Countable Open Covers Condition for Separated Sets

Let $T = \struct {S, \tau}$ be a topological space.
Let $A, B \subseteq S$
For all $X \subseteq S$, let $X^-$ denote the closure of $X$ in $T$.
Let:
:$\UU = \set {U_n : n \in \N}$ be a countable open cover of $A : \forall n \in \N : {U_n}^- \cap B = \O$
Let:
:$\VV = \set {V_n : n \in \N}$ be a countable open cover of $B : \forall n \in \N : {V_n}^- \cap A = \O$
Then:
:$A$ and $B$ can be separated in $T$

Proof:
By definition of cover:
:$\ds A \subseteq \bigcup_{n \mathop \in \N} U_n$
We have:
:$\ds A \cap \paren{\bigcup_{n \mathop \in \N} {V_n}^-} = \O$
From Subset of Set Difference iff Disjoint Set:
:$(1): \quad \ds A \subseteq \paren {\bigcup_{n \mathop \in \N} U_n} \setminus \paren {\bigcup_{n \mathop \in \N} {V_n}^-}$
Similarly:
:$(2): \quad \ds B \subseteq \paren {\bigcup_{n \mathop \in \N} V_n} \setminus \paren {\bigcup_{n \mathop \in \N} {U_n}^-}$
For each $n \in \N$, let:
:${U_n}' = U_n \setminus \paren {\ds \bigcup_{p \mathop \le n} {V_p}^-}$
For each $n \in \N$, let:
:${V_n}' = V_n \setminus \paren {\ds \bigcup_{p \mathop \le n} {U_p}^-}$
Theorem: Countable Open Covers Condition for Separated Sets/Lemma 1

:$\forall n, m \in \N : {U_n}' \cap {V_m}' = \O$

Proof:
Let $n, m \in \N$.
{{WLOG}}, let $m \le n$.
We have:
{{begin-eqn}}
{{eqn | l = {U_m}'
      | r = U_m \setminus \paren {\bigcup_{p \mathop \le m} {V_p}^-}
      | c = Definition of ${U_m}'$
}}
{{eqn | o = \subseteq 
      | r = U_m 
      | c = Set Difference is Subset
}}
{{eqn | o = \subseteq 
      | r = {U_m}^- 
      | c = Set is Subset of its Topological Closure
}}
{{end-eqn}}
As $m \le n$, then:
:${U_m}^- \in \set { {U_p}^- : p \le n}$
We have:
{{begin-eqn}}
{{eqn | l = U_m^-
      | o = \subseteq
      | r = \bigcup_{p \mathop \le n} {U_p}^-
      | c = Set is Subset of Union
}}
{{end-eqn}}
Also:
{{begin-eqn}}
{{eqn | l = {V_n}'
      | r = V_n \setminus \paren {\bigcup_{p \mathop \le n} {U_p}^-}
      | c = Definition of ${V_m}'$
}}
{{eqn | o = \subseteq 
      | r = V_n \setminus {U_m}^-
      | c = Set Difference with Subset is Superset of Set Difference
}}
{{end-eqn}}
Finally:
{{begin-eqn}}
{{eqn | l = {U_m}' \cap {V_n}'
      | r = \paren {U_m \setminus \paren {\bigcup_{p \mathop \le m} {V_p}^-} } \cap \paren {V_n \setminus \paren {\bigcup_{p \mathop \le n} {U_p}^-} }
}}
{{eqn | o = \subseteq 
      | r = {U_m}^- \cap \paren {V_n \setminus {U_m}^-}
      | c = Set Intersection Preserves Subsets
}}
{{eqn | r = \O
      | c = Set Difference Intersection with Second Set is Empty Set
}}
{{end-eqn}}
From Empty Set is Subset of All Sets:
:$\O \subseteq {U_m}' \cap {V_n}'$
By definition of set equality:
:${U_m}' \cap {V_n}' = \O$
Similarly:
:${U_n}' \cap {V_m}' = \O$
The result follows.
{{qed}}
Category:Countable Open Covers Condition for Separated Sets
krnzp0smunwocw1evdvyy9tw57usg4j
Theorem: Countable Open Covers Condition for Separated Sets/Lemma 2

:$U$ and $V$ are open in $T$.

Proof:
By {{Open-set-axiom|2}}, it is sufficient to show that:
:$\forall n \in \N : {U_n}', {V_n}' \in \tau$
Let  $n \in \N$.
We have:
{{begin-eqn}}
{{eqn | l = {U_n}'
      | r = U_n \setminus \paren {\ds \bigcup_{p \mathop \le n} {V_p}^-}
      | c = Definition of ${U_n}'$
}}
{{eqn | r = U_n \cap \relcomp S {\bigcup_{p \mathop \le n} {V_p}^-}
      | c = Set Difference as Intersection with Relative Complement
}}
{{eqn | r = U_n \cap \paren{ \bigcap_{p \mathop \le n} \relcomp S { {V_p}^-} }
      | c = De Morgan's laws
}}
{{end-eqn}}
From Topological Closure is Closed:
:${V_p}^-$ is a closed set.
By definition of closed set:
:$\relcomp S {V_p^-}$ is an open set.
Hence:
:${U_n}'$ is the finite intersection of open sets.
By {{Open-set-axiom|3}}:
:${U_n}'$ is an open set.
Similarly:
:${V_n}'$ is an open set.
The result follows from {{Open-set-axiom|2}}.
{{qed}}
Category:Countable Open Covers Condition for Separated Sets
qabjtkn3kut4x1y6fj0ljbs0f947k67
Theorem: Square Function is Even

The square function:
:$\map f x = x^2$
is an even function.

Proof:
{{begin-eqn}}
{{eqn | q = \forall x \in \R
      | l = \paren {-x}^2
      | r = \paren {-x} \times \paren {-x}
      | c = 
}}
{{eqn | r = \paren {-1}^2 x^2
      | c = 
}}
{{eqn | r = x^2
      | c = 
}}
{{end-eqn}}
Hence the result by definition of even function.
{{qed}}
Theorem: Subset of Locally Finite Set of Subsets is Locally Finite

Let $T = \struct {S, \tau}$ be a topological space.
Let $\FF \subseteq \powerset S$ be a set of subsets of $S$.
Let $\GG \subseteq \FF$.
If $\FF$ is locally finite then $\GG$ is locally finite.

Proof:
We prove the contrapositive statement:
:If $\GG$ is not locally finite then $\FF$ is not locally finite.
Let $\GG$ not be locally finite.
By definition of locally finite:
:$\exists x \in S : \forall N \subseteq S : N$ is a neighborhood of $x : N$ intersects an infinite number of sets in $\GG$.
By definition of subset:
:$\forall X \in \GG : X \in \FF$
Hence:
:$\exists x \in S : \forall N \subseteq S : N$ is a neighborhood of $x : N$ intersects an infinite number of sets in $\FF$.
By definition, $\FF$ is not locally finite.
The result follows from Rule of Transposition.
{{qed}}
Category:Locally Finite Sets of Subsets
1yymivou2rfn2vyo1knlsgckio9dq10
Theorem: Cube Function is Odd

The cube function on the real numbers:
:$\forall x \in \R: \map f x = x^3$
is an odd function.

Proof:
{{begin-eqn}}
{{eqn | q = \forall x \in \R
      | l = \paren {-x}^3
      | r = \paren {-1}^3 x^3
      | c = 
}}
{{eqn | r = -x^3
      | c = 
}}
{{end-eqn}}
Hence the result by definition of odd function.
{{qed}}