avewright/proofwiki-math huggingface dataset:
Theorem: Direction of Line of Electric Force

Let $\mathbf E$ be an electric field.
Let $L$ be a '''line of force''' within $\mathbf E$.
Then $L$ has one of the following properties:
:$(1): \quad$ Begins on a positively charged body and ends on a negatively charged body
:$(2): \quad$ Begins on a positively charged body and goes to infinity without terminating
:$(3): \quad$ Comes from infinity without a start point and ends on a negatively charged body.

Proof:
{{ProofWanted|Not sure if this is something you can prove or whether it's a physical law. Grant and Phillips state it without elaboration.}}
Theorem: Line of Electric Force is Continuous

Let $\mathbf E$ be an electric field.
Let $L$ be a '''line of force''' within $\mathbf E$.
Then, except for the positive charge or negative charge at which $L$ may start or end, $L$ is continuous.

Proof:
Follows directly from Vector Line is Continuous.
Theorem: Lines of Electric Force do not Cross

Let $\mathbf E$ be an electric field.
Let $L_1$ and $L_2$ be '''lines of force''' within $\mathbf E$.
Then $L_1$ and $L_2$ do not cross over each other.

Proof:
Follows directly from Vector Lines do not Intersect.
Theorem: Recursive Set is Turing Computable

Let $f: S \to \set {0, 1}$, where $S \subseteq \N$, be a recursive function.
Let $\sqbrk x$ denote the reverse of the base-$2$ representation of $x$, possibly with additional $0$ at the end.
:That is, if the base-$2$ representation of $x$ is
::$\sqbrk {r_m r_{m - 1} \dotsm r_1 r_0}_2$
:then $\sqbrk x$ is:
::$r_0 r_1 \dotsm r_{m - 1} r_m 0 \dotsm 0$
There exists a Turing machine such that:
* The input symbols of the machine are $\set {0, 1}$
* The machine accepts the language $\set {\sqbrk x : \map f x = 1}$
* The machine halts on $\sqbrk x$ {{iff}} $x \in S$

Proof:
{{Proofread}}
By Recursive Function is URM Computable, there is a URM program that computes $f$.
By Normalized URM Program, let $P$ be the normalization of it.
Let $k = \map \rho P$ be the highest register number used by $P$.
Construct the $k + 1$-tape Turing machine $T$ as follows, where $\map \rho P$ is the highest register number used by $P$.
For the purposes of this proof, the tapes will be labeled from $0$ to $k$.
Theorem: Signum Complement Function is Primitive Recursive

Let $\overline \sgn: \N \to \N$ by defined as the signum-bar function.
Then $\overline \sgn$ is primitive recursive.

Proof:
From Signum Complement Function on Natural Numbers as Characteristic Function, $\map {\overline \sgn} n = \chi_{\set 0} n$.
From Set Containing Only Zero is Primitive Recursive, $\chi_{\set 0}$ is primitive recursive.
Hence the result.
{{qed}}
Category:Signum Function
Category:Primitive Recursive Functions
okzns6v9dhc9ef79e2ssjzpk001tfqo
Theorem: Basis Representation is Primitive Recursive

Let $\operatorname{basis} : \N^3 \to \N$ be defined as follows:
:$\map {\operatorname{basis} } {b, n, i} = \begin{cases}
1 & : b = 1 \land i < n \\
r_i & : b > 1 \land i \le m \\
0 & : \text {otherwise}
\end{cases}$
where $\sqbrk {r_m r_{m - 1} \dots r_1 r_0}_b$ is the base-$b$ representation of $n$.

Proof:
Consider the following function:
:$\map f {b, n, i} = \begin{cases}
n & : i = 0 \\
\map {\operatorname{quot} } {\map f {b, n, i - 1}, b} & : i > 0
\end{cases}$
As $f$ is obtained by Primitive Recursion and:
* Constant Function is Primitive Recursive
* Quotient is Primitive Recursive
Thus, $f$ is primitive recursive.
Observe that $\map f {b, n, 0} = n$ which is the number represented by $\sqbrk {r_m r_{m - 1} \dots r_1 r_0}_b$.
Now, suppose that $\map f {b, n, i}$ is the number represented by $\sqbrk {r_m r_{m - 1} \dots r_{i + 1} r_i}_b$.
Then:
{{begin-eqn}}
{{eqn | l = \map f {b, n, i + 1}
      | r = \map {\operatorname{quot} } {\sqbrk {r_m r_{m - 1} \dots r_{i + 1}, r_i}_b, b}
      | c = Definition of $f$
}}
{{eqn | r = \map {\operatorname{quot} } {\sum_{j = 0}^{m - i} r_{j + i} b^j, b}
      | c = Basis Representation Theorem
}}
{{eqn | r = \map {\operatorname{quot} } {r_i + \sum_{j = 0}^{m - i - 1} r_{j + i + 1} b^{j + 1}, b}
}}
{{eqn | r = \map {\operatorname{quot} } {r_i + b \sum_{j = 0}^{m - i - 1} r_{j + i + 1} b^j, b}
}}
{{eqn | r = \sum_{j = 0}^{m - i - 1} r_{j + i + 1} b^j
      | c = Division Theorem
}}
{{eqn | r = \sqbrk {r_m r_{m - 1} \dots r_{i + 2} r_{i + 1} }_b
      | c = Basis Representation Theorem
}}
{{end-eqn}}
Thus, by Principle of Mathematical Induction:
:$\map f {b, n, i} = \sqbrk {r_m r_{m - 1} \dots r_{i + 1} r_i}$
Define $\map g {b, n, i} = \map {\operatorname{rem} } {\map f {b, n, i}, b}$.
Then $g$ is primitive recursive, since Remainder is Primitive Recursive.
For each $i$:
{{begin-eqn}}
{{eqn | l = \map g {b, n, i}
      | r = \map {\operatorname{rem} } {\map f {b, n, i}, b}
}}
{{eqn | r = \map {\operatorname{rem} } {\sqbrk {r_m r_{m - 1} \dots r_{i + 1} r_i}, b}
}}
{{eqn | r = \map {\operatorname{rem} } {\sum_{j = 0}^{m - i} r_{j + i} b^j, b}
      | c = Division Theorem
}}
{{eqn | r = \map {\operatorname{rem} } {r_i + b \sum_{j = 0}^{m - i - 1} r_{j + i + 1} b^j, b}
}}
{{eqn | r = r_i
      | c = Division Theorem
}}
{{end-eqn}}
The result follows from:
* Definition by Cases is Primitive Recursive
* Ordering Relations are Primitive Recursive
* Set Operations on Primitive Recursive Relations
* Constant Function is Primitive Recursive
{{qed}}
Category:Primitive Recursive Functions
n6rbwkd1f48vuaiha3v1ruk0xyywfio
Theorem: Nagata-Smirnov Metrization Theorem/Necessary Condition

A metrizable topological space $T = \struct {S, \tau}$ is regular and has a basis that is $\sigma$-locally finite.

Proof:
==== $T$ is Regular ====
We show that $T$ is regular.
{{Recall|Metrizable Space|metrizable space|index = 1}}
{{:Definition:Metrizable Space/Definition 1}}
From Metric Space is Regular Space:
:$T$ is a regular space.
{{qed|lemma}}
{{improve|We can replace the rest of this with Pseudometrizable Space has Sigma-Locally Finite Basis}}
==== Construction of Basis $\VV$ ====
We construct a $\sigma$-locally finite basis $\VV$.
For each $n \in \N$, let:
:$\UU_n = \set{\map {B_{1 / 2^n}} x : x \in S}$
That is, $\UU_n$ is the set of all open balls of radius $\dfrac 1 {2^n}$.
From Open Balls of Same Radius form Open Cover:
:$\forall n \in \N: \UU_n$ is an open cover of $T$
From Metric Space is Paracompact:
:$T$ is a paracompact space
By definition of paracompact space:
:$\forall n \in \N : \exists$ a open refinement $\VV_n$ of $\UU_n$ which is locally finite
Let $\VV = \ds \bigcup_{n \in \N} \VV_n$.
By definition, $\VV$ is $\sigma$-locally finite.
==== $\VV$ is Basis ====
We show that $\VV$ is a basis.
Let $U \in \tau$.
Let $x \in U$.
From Sequence of Powers of Number less than One:
:the sequence $\sequence{\dfrac 1 {2^n}}$ is a null sequence
From Null Sequence induces Local Basis in Metric Space:
:$\exists n \in N : \map {B_{1 / 2^n}} x \subseteq U$
By definition of open refinement:
:$\VV_{n + 1}$ is an open cover
By definition of open cover:
:$\exists V \in \VV_{n + 1} : x \in V$
By definition of open refinement:
:$\exists U \in \UU_{n + 1} : V \subseteq U$
By definition of $\UU_{n + 1}$:
:$\exists y \in S : U = \map {B_{1 / 2^{n + 1}}} y$
We have:
:$x \in V \subseteq \map {B_{1 / 2^{n + 1}}} y$
From Open Ball Contains Open Ball Less Than Half Its Radius:
:$\map {B_{1 / {2^{n + 1}}}} y \subseteq \map {B_{1 / 2^n}} x$
Hence:
:$x \in V \subseteq \map {B_{1 / {2^{n + 1}}}} y \subseteq \map {B_{1 / 2^n}} x$
By definition $\VV$ is a basis.
Hence $\VV$ is a basis that is $\sigma$-locally finite.
Theorem: Total Charge carried By Electron in Hydrogen Atom

Consider an atom of hydrogen $\mathrm H$.
Then:
:$\ds \int_V \map {\rho_{\mathrm {el} } } {\mathbf r} \rd \tau = -\E$
where:
:$\d \tau$ is an infinitesimal volume element
:$\mathbf r$ is the position vector of $\d \tau$
:$V$ is a volume large enough to completely enclose $\mathrm H$
:$\map {\rho_{\mathrm {el} } } {\mathbf r}$ is the electric charge density caused by the charge on the electron in the electron cloud at $\mathbf r$
:$\E$ is the elementary charge.

Proof:
The total electric charge on $\mathrm H$ carried by the electron is equal to the total charge on the electron.
By definition of the charge on the electron, this total is $-\E$.
The result follows.
{{qed}}
Theorem: Total Charge carried By Electron in Hydrogen Atom/Cartesian Form

The total electric charge on $\mathrm H$ carried by the electron can be expressed in Cartesian coordinates as:
{{begin-eqn}}
{{eqn | l = \int_{\text {all space} } \map {\rho_{\mathrm {el} } } {\mathbf r} \rd \tau
      | r = 
      | c = 
}}
{{eqn | l = \int_{-\infty}^\infty \int_{-\infty}^\infty \int_{-\infty}^\infty \map {\rho_{\mathrm {el} } } {\mathbf r} \rd x \rd y \rd z
      | r = -\E
      | c = 
}}
{{end-eqn}}

Proof:
Follows directly.
{{qed}}
Theorem: Binary Sequence Codes are Primitive Recursive

The following function is primitive recursive:
:$\map {\operatorname{bincode} } {n, i} = o_i$
where $o_i$ is the number of $1$ digits between the $i - 1$-th and $i$-th $0$ digit in the base-$2$ representation of $n$, starting from the least significant digits.
As a special case, $\map {\operatorname{bincode} } {n, 0}$ is the number of $1$ digits before the first $0$ digit.
In other words, suppose the base-$2$ representation of $n$ is:
:$\sqbrk {\dots 1 1 \dots 1 1 0 1 1 \dots 1 1 0 1 1 \dots 1 1}$
Then $\map {\operatorname{bincode} } {n, i}$ is the length of the $i + 1$-th string of $1$ digits, counting from the right.

Proof:
By Basis Representation is Primitive Recursive, we have that $\map {\operatorname{basis} } {b, n, i}$ is primitive recursive.
Consider the function:
:$\map z {n, i} = \begin{cases}
\map {\mu j < n} {\map {\operatorname{basis} } {2, n, j} = 0} & : i = 0 \\
\map {\mu j < n} {j > \map z {n, i - 1} \land \map {\operatorname{basis} } {2, n, j} = 0} & : i > 0
\end{cases}$
It returns the position of the $i + 1$-th $0$ in the base-$2$ representation of $n$.
If the digit exists, it will always be found, as the base-$2$ representation is never longer than $n$.
If there is no such digit, then it returns a position beyond the representation.
In particular, consecutive values of $z$ that are beyond its length will always be at most $1$ apart, and increasing.
Additionally $z$, is primitive recursive, as:
* Constant Function is Primitive Recursive
* Equality Relation is Primitive Recursive
* Ordering Relations are Primitive Recursive
* Bounded Minimization is Primitive Recursive
and it is obtained by primitive recursion on them.
Then:
:$\map {\operatorname{bincode} } {n, i} = \begin{cases}
\map z {n, 0} & : i = 0 \\
\map z {n, i} - \map z {n, i - 1} - 1 & : i > 0
\end{cases}$
which is primitive recursive by:
* Definition by Cases is Primitive Recursive
* Cut-Off Subtraction is Primitive Recursive
in addition to the above.
{{qed}}
Category:Primitive Recursive Functions
crauuq7xb1wpt9foazkuk79es077bgp
Theorem: Straight Line Segment is Shortest Path between Two Points

Let $A$ and $B$ be distinct points in a Euclidean space.
Let $\LL$ be the straight line segment lying on both $A$ and $B$.
Then $\LL$ is the shortest line that lies on both $A$ and $B$.

Proof:
Let $A = \tuple {x_1, y_1}$ and $B = \tuple {x_2, y_2}$ be an arbitrary pair of distinct points embedded in the Cartesian $\R^2$-plane.
Let $\LL$ be the straight line segment from $A$ to $B$.
We are to demonstrate that there does not exist a differentiable real function $f: \R \to \R$ such that:
{{begin-eqn}}
{{eqn | l = \map f {x_1}
      | r = y_1
}}
{{eqn | l = \map f {x_2}
      | r = y_2
}}
{{end-eqn}}
and such that the arc length of the graph of $f$ from $A$ to $B$ is less than the length of $\LL$.
Note that for $x_1 = x_2$, a similar argument can applied to a function $\map f y$.
The proof relies on the Fundamental Theorem of Calculus and the definition of the the arc length of a differentiable real function.
{{AimForCont}} there exists a real function $f: \R \to \R$ such that:
:$\map f {x_1} = y_1$ and $\map f {x_2} = y_2$
and such that:
:the arc length of the graph of $f$ from $A$ to $B$ is less than the length of $\LL$.
This means that $\map f x$ is continuous over $\closedint {x_1} {x_2}$ (and for the sake of the proof, differentiable over the same interval).
{{explain|How do we know that there is no real-valued function passing through $A$ and $B$ which is not differentiable? All this proof does is show that a differentiable function has the required property.}}
Thus, the arc length of the graph of $\map f x$ over $\closedint {x_1} {x_2}$ is:
:$\ds L_f = \int_{x_1}^{x_2} \sqrt {1 + \paren {\map {f'} x}^2} \rd x$
Suppose that $L_f$ is less than the length of the line connecting $\tuple {x_1, y_1}$ and $\tuple {x_2, y_2}$.
We have that Slope of Tangent to Curve at Point equals Value of Derivative, which we will denote $s$.
Thus, the length of the line is given by:
:$L_l = \ds \int_{x_1}^{x_2} \sqrt {1 + s^2} \rd x$
where $s = \dfrac {y_2 - y_1} {x_2 - x_1}$.
Since $L_f < L_l$, transitively, we have that:
:$\ds \int_{x_1}^{x_2} \sqrt {1 + \paren {\map {f'} x}^2} \rd x < \int_{x_1}^{x_2} \sqrt {1 + s^2} \rd x$
Theorem: Discrete Normal Subgroup of Connected Group is Contained in Center

Let $G$ be a connected topological group.
Let $\map Z G$ be the center of $G$.
Let $N$ be a discrete normal subgroup of $G$.
Then:
:$N \subseteq \map Z G$

Proof:
Let $h \in N$.
We shall show $h \in \map Z G$
Now, let:
:$A _h := \set {g \in G : g^{-1} h g = h}$
Then, we need to show:
:$A _h = G$
Let $e \in G$ denote the identity.
Since $e \in A _h$, we have $A _h \ne \O$.
Thus, it suffices to show that $A _h$ is clopen in view of {{Defof|Connected Topological Space|index = 4}}.
As $N$ is a discrete subgroup, there is an open set $U \subseteq G$ such that:
:$U \cap N = \set e$
Multiplying the above equality from left, we also have:
:$\forall h \in N : h U \cap N = \set h$
Define $\phi _h : G \to N$ by:
:$\map {\phi _h} g := g^{-1} h g$
Then $\phi _h$ is continuous.
Thus both:
{{begin-eqn}}
{{eqn | l = A _h
      | r = \set {g \in G : g^{-1} h g \in h U }
}}
{{eqn | r = \phi _h^{-1} \sqbrk {h U}
}}
{{end-eqn}}
and
{{begin-eqn}}
{{eqn | l = G \setminus A _h
      | r = \set {g \in G : g^{-1} h g \not \in h U }
}}
{{eqn | r = \bigcup _{h' \in N \setminus \set h} \phi _h^{-1} \sqbrk {h' U}
}}
{{end-eqn}}
are open.
That is, $A _h$ is clopen.
{{Finish|More details}}
Category:Topological Groups
90ekd1vz9euc25xlaokixntv69wf6ei
Theorem: Length of Binary Sequence Code is Primitive Recursive

Let the function $\map {\operatorname{bincodelen} } n$ be defined as the least $m$ such that:
:For every $i \ge m$, $\map {\operatorname{bincode} } {n, i} = 0$
where $\operatorname{bincode}$ is defined as in Binary Sequence Codes are Primitive Recursive.
Then, $\operatorname{bincodelen}$ is primitive recursive.

Proof:
The base-$2$ representation of $n$ is never longer than $n$ digits.
Therefore, there are at most $n$ digits that are $0$.
By definition of $\operatorname{bincode}$, there are thus at most $n$ nonzero values.
Thus, the following definition is correct:
:$\map {\operatorname{bincodelen} } n = \map {\mu m \le n} {\map {\mu i \le n} {i \ge m \land \map {\operatorname{bincode} } {n, i} \ne 0} > n}$
For, the inner minimization attempts to find some counterexample $i$ to the proposition that $m$ is the value of the function, as defined.
If no such counterexample is found, by the definition of bounded minimization, the result is $n + 1 > n$.
It follows from:
* Binary Sequence Codes are Primitive Recursive
* Set Operations on Primitive Recursive Relations
* Ordering Relations are Primitive Recursive
* Bounded Minimization is Primitive Recursive
* Equality Relation is Primitive Recursive
that $\operatorname{bincodelen}$ is primitive recursive.
{{qed}}
Category:Primitive Recursive Functions
fsfwt1zr4gnarttvkvptsaztgchuair
Theorem: Recursive Relation is Turing Computable

Let $f: S \to \set {0, 1}$, where $S \subseteq \N^k$ be a recursive function.
Let the encoding of some $\tuple {x_1, x_2, \dotsc, x_k} \in \N^k$ be the string:
:$1^{x_1} 0 1^{x_2} 0 1^{x_3} 0 \dotsm 0 1^{x_k}$
Then, there exists a Turing machine such that:
* The input symbols of the machine are $\set {0, 1}$
* The accepted language is the set of encodings of $\tuple {x_1, x_2, \dotsc, x_k}$ such that $\map f {x_1, x_2, \dotsc, x_k} = 1$
* The machine halts on an input {{iff}} it is not in the correct format, or it is the encoding of some $\tuple {x_1, x_2, \dotsc, x_k}$ such that $\map f {x_1, x_2, \dotsc, x_k}$ is defined

Proof:
Define the function $g: S' \to \set {0, 1}$, where $S \subseteq \N$, as follows:
:$\map g x = \map f {\map {\operatorname{bincode} } {x, 0}, \map {\operatorname{bincode} } {x, 1}, \dotsc, \map {\operatorname{bincode} } {x, k} }$
That is, assuming the input is properly formatted, $g$ takes the value of $f$ when applied to the lengths of the strings of $1$ digits in the base-$2$ representation of the input.
Additionally, from:
* Constant Function is Primitive Recursive
* Primitive Recursive Function is Total Recursive Function
it follows that $g$ is recursive, as it is obtained by substitution on $f$ and other recursive functions.
By Recursive Set is Turing Computable, there exists a Turing machine $T_g$ that computes $g$.
The input is properly formatted {{iff}} it contains exactly $k - 1$ instances of $0$.
By Symbol Count by Finite State Machine, there is a finite state machine $F$ that accepts {{iff}} the number of $0$ symbols in the input is $k - 1$.
By Finite State Machine is Turing Computable, there is a Turing machine $T_F$ that always halts, which performs the same check.
The result follows from Intersection of Turing Machines with $T_g$ and $T_F$.
{{qed}}
Category:Recursive Functions
Category:Turing Machines
szgh4sod0swm29c75e3avug0byis78w
Theorem: Recursive Relation is Turing Computable/Corollary

Let $f: S \to \set {0, 1}$, where $S \subseteq \N$ be a recursive function.
Let $x \in \N$ be encoded as:
:$1 1 \dotsm 1$
where $1$ is repeated $x$ times.
Then there exists a Turing machine such that:
* The input symbols of the machine are $\set 1$
* The accepted language are the encodings of $x \in \N$ such that $\map f x = 1$
* The machine halts on an input {{iff}} it is the encoding for some $x \in \N$ such that $\map f x$ is defined

Proof:
By Recursive Relation is Turing Computable, there is a Turing machine $T$ that satisfies the conditions.
The result follows from an identical machine, except that the input symbols are restricted to be only $\set 1$.
{{qed}}
Category:Recursive Functions
Category:Turing Machines
7cg3pk55p5mps73ne6aprqammb1023m
Theorem: Atomic Electric Field at Point within Body of Matter

Let $B$ be a body of matter.
Let $P$ be a point inside $B$ whose position vector is $\mathbf r$.
The '''atomic electric field''' at $P$ is given by:
:$\ds \map {\mathbf E_{\text {atomic} } } {\mathbf r} = \dfrac 1 {4 \pi \varepsilon_0} \int_{\text {all space} } \dfrac {\paren {\mathbf r - \mathbf r'} \map {\rho_{\text {atomic} } } {\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_{\mathrm {atomic} } } {\mathbf r'}$ is the atomic charge density caused by the electric charges within the atoms that make up $B$
:$\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 atomic charge density and convert the summation into a definite integral, as follows:
Consider an infinitesimal volume element $\d V'$:
: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 electric charge density:
:$\map {\rho_{\mathrm {atomic} } } {\mathbf r'} = \dfrac {\d q} {\d V'}$
and so:
:$\map {\mathbf E_{\text {atomic} } } {\mathbf r'} = \dfrac 1 {4 \pi \epsilon_0} \dfrac {\paren {\mathbf r - \mathbf r'} \map {\rho_{\mathrm {atomic} } } {\mathbf r'} } {\size {\mathbf r - \mathbf r'}^3} \rd V'$
Integrating over all space:
:$\ds \map {\mathbf E_{\text {atomic} } } {\mathbf r} = \dfrac 1 {4 \pi \varepsilon_0} \int_{\text {all space} } \dfrac {\paren {\mathbf r - \mathbf r'} \map {\rho_{\text {atomic} } } {\mathbf r'} } {\size {\mathbf r - \mathbf r'}^3} \rd V'$
Hence the result.
{{qed}}
Theorem: Equivalence of Definitions of Cover of Set

Let $S$ be a set.
{{TFAE|def = Cover of Set}}

Proof:
=== Definition 1 Implies Definition 2 ===
Let $\CC$ be a set of sets such that:
:$\ds S \subseteq \bigcup \CC$
where $\bigcup \CC$ denotes the union of $\CC$.
By definition of subset:
:$\forall s \in S : s \in \ds \bigcup \CC$
By definition of set union:
:$\forall s \in S : \exists C \in \CC : s \in C$
{{qed|lemma}}
Theorem: Unbounded Space Minus Bounded Space is Unbounded

Let $M$ be a metric space.
Let $A \subseteq M$ be unbounded in $M$.
Let $B \subseteq M$ be bounded in $M$.
Then $A \setminus B$ is unbounded in $M$.

Proof:
{{AimForCont}} $A \setminus B$ is bounded.
Then by definition of bounded:
:$\exists K \in \R: \forall x, y \in A \setminus B: \map d {x, y} \le K$
By definition of bounded, choose some $a_b \in A$ and $d_b \in \R$ such that:
:$\forall x \in B: \map d {x, a_b} \le d_b$
By definition of unbounded, $A$ is not bounded is $M$.
Thus, by the negation of the definition of bounded:
:$\exists a_x \in A: \map d {a_x, a_b} > d_b$
Let $d_x = \map d {a_x, a_b}$.
Again, by the negation of the definition of bounded:
:$\exists a_y \in A: \map d {a_y, a_b} > d_x + K$
Let $d_y = \map d {a_y, a_b}$.
As $\map d {a_x, a_b} > d_b$, it follows that $a_x \notin B$.
Likewise, as $\map d {a_y, a_b} > d_x > d_b$, $a_y \notin B$.
Thus, both $a_x, a_y \in A \setminus B$.
But:
{{begin-eqn}}
{{eqn | l = \map d {a_y, a_x}
      | o = \ge
      | r = \size {\map d {a_b, a_y} - \map d {a_b, a_x} }
      | c = Reverse Triangle Inequality
}}
{{eqn | r = \size {d_y - d_x}
}}
{{eqn | r = d_y - d_x
      | c = As $d_y > d_x$
}}
{{eqn | o = >
      | r = d_x + K - d_x
}}
{{eqn | r = K
}}
{{end-eqn}}
Then, $a_y, a_x \in A \setminus B$ are two points such that $\map d {a_y, a_x} > K$, contradicting our assumption.
Thus, by Proof by Contradiction, it follows that $A \setminus B$ is unbounded.
{{qed}}
Theorem: Unbounded Space Minus Bounded Space is Unbounded

Let $M$ be a metric space.
Let $A \subseteq M$ be unbounded in $M$.
Let $B \subseteq M$ be bounded in $M$.
Then $A \setminus B$ is unbounded in $M$.

Proof:
{{AimForCont}} $A \setminus B$ is bounded.
By Finite Union of Bounded Subsets:
:$\paren {A \setminus B} \cup B$
is bounded.
On the other hand, by {{Defof|Set Difference}}:
:$A \subseteq \paren {A \setminus B} \cup B$
Thus by Subset of Bounded Subset of Metric Space is Bounded, $A$ must be bounded, too.
This is a contradiction.
{{qed}}
Theorem: Distribution of Macroscopic Electric Charge within Insulator

Let $B$ be a body made out of an electrically insulating substance.
Then it is possible for different volume elements of $B$ to have different (macroscopic) electric fields caused by intrinsic imbalance of the electric charges distributed throughout $B$.

Proof:
In an electrical insulator, electric charges cannot flow, because of the nature of the substance.
Hence an electric charge in one point within $B$ cannot flow to another point within $B$ under a potential difference caused by the presence of those (macroscopic) electric fields.
{{qed}}