avewright/proofwiki-math huggingface dataset:
Theorem: Characterization of Paracompactness in T3 Space/Lemma 5

:$\forall V \in \VV: V \subseteq V^*$

Proof:
Let $V \in \VV$.
Let $\AA_V = \set{A \in \AA | A \cap V = \O}$.
From Subset of Set Difference iff Disjoint Set:
:$\forall A \in \AA_V : V \subseteq X \setminus A$
We have:
{{begin-eqn}}
{{eqn | l = V
      | o = \subseteq
      | r = \bigcap \set{X \setminus A : A \in \AA_V}
      | c = Set is Subset of Intersection of Supersets
}}
{{eqn | r = X \setminus \bigcup \set{A : A \in \AA_V}
      | c = De Morgan's Laws for Set Difference
}}
{{eqn | r = V^*
      | c = definition of $V^*$
}}
{{end-eqn}}
{{qed}}
Category:Characterization of Paracompactness in T3 Space
c9knp0t9p2xzg87i3btqvj91wvyt3yz
Theorem: Basic Primitive Recursive Functions are Arithmetically Definable

Let $f: \N^k \to \N$ be a basic primitive recursive function.
Then there is a WFF $\map \phi {y, x_1, \dotsc, x_k}$ of $k + 1$ free variables and no quantifiers such that:
:$y = \map f {x_1, \dotsc, x_k}$
{{iff}}
:$\N \models \map \phi {y \gets \sqbrk y, x_1 \gets \sqbrk {x_1}, \dotsc, x_k \gets \sqbrk {x_k} }$
where $\sqbrk a$ denotes the unary representation of $a \in \N$.

Proof:
=== Zero Function ===
Suppose $\map f x = 0$.
Then:
:$\map \phi {y, x} := y = 0$
Correctness is apparent.
{{qed|lemma}}
Theorem: Substitution of Arithmetically Definable Functions is Arithmetically Definable

Let $f: \N^t \to \N$ and $g_1, g_2, \dotsc, g_t: \N^k \to \N$ be partial functions.
Let $h: \N^k \to \N$ be defined by substitution as:
:$\map h {x_1, \dotsc, x_k} \approx \map f {\map {g_1} {x_1, \dotsc, x_k}, \dotsc, \map {g_t} {x_1, \dotsc, x_k} }$ 
Suppose that there exists a $\Sigma_1$ WFF of $t + 1$ free variables:
:$\map {\phi_f} {y, x_1, \dotsc, x_t}$
such that:
:$y = \map f {x_1, \dotsc, x_t} \iff \N \models \map {\phi_f} {\sqbrk y, \sqbrk {x_1}, \dotsc, \sqbrk {x_t} }$
where $\sqbrk a$ denotes the unary representation of $a \in \N$.
Suppose also that there exist $\Sigma_1$ WFFs of $k + 1$ free variables:
:$\map {\phi_{g_1} } {y, x_1, \dotsc, x_k}$
:$\dots$
:$\map {\phi_{g_t} } {y, x_1, \dotsc, x_k}$
such that:
:$y = \map {g_i} {x_1, \dotsc, x_k} \iff \N \models \map {\phi_{g_i} } {\sqbrk y, \sqbrk {x_1}, \dotsc, \sqbrk {x_k} }$
for each $1 \le i \le t$.
Then there exists a $\Sigma_1$ WFF of $k + 1$ free variables:
:$\map {\phi_h} {y, x_1, \dotsc, x_k}$
such that:
:$y = \map h {x_1, \dotsc, x_k} \iff \N \models \map {\phi_h} {\sqbrk y, \sqbrk {x_1}, \dotsc, \sqbrk {x_k} }$

Proof:
Define:
:$\map {\phi_h} {y, x_1, \dotsc, x_k} := \exists s_1: \dotsm \exists s_t: \map {\phi_f} {y, s_1, \dotsc, s_t} \land \map {\phi_{g_1} } {s_1, x_1, \dotsc, x_k} \land \dotso \land \map {\phi_{g_t} } {s_t, x_1, \dotsc, x_k}$
Correctness is apparent.
{{TheoremWanted|$\paren {\exists x: \map \phi x} \land \psi \vdash \exists x: \paren {\map \phi x \land \psi}$}}
That $\phi_h$ is $\Sigma_1$ follows from Conjunction of Existential Quantifier.
{{qed}}
Category:Primitive Recursive Functions
qirugxuj6pdrd5ako1t1aki4astnx68
Theorem: Minimization of Arithmetically Definable Function is Arithmetically Definable

Let $f: \N^{k + 1} \to \N$ be a partial function.
Let $g: \N^k \to \N$ be the partial function defined as:
:$\map g {x_1, \dotsc, x_k} \approx \map {\mu z} {\map f {x_1, \dotsc, x_k, z} }$
where $\mu$ is minimization.
Suppose that there exists a $\Sigma_1$ WFF of $k + 2$ free variables:
:$\map {\phi_f} {y, x_1, \dotsc, x_k, z}$
such that:
:$y = \map f {x_1, \dotsc, x_k, z} \iff \N \models \map {\phi_f} {\sqbrk y, \sqbrk {x_1}, \dotsc, \sqbrk {x_k}, \sqbrk z}$
where $\sqbrk a$ denotes the unary representation of $a \in \N$.
Then there exists a $\Sigma_1$ WFF of $k + 1$ free variables:
:$\map {\phi_g} {y, x_1, \dotsc, x_k}$
such that:
:$y = \map g {x_1, \dotsc, x_k} \iff \N \models \map {\phi_g} {\sqbrk y, \sqbrk {x_1}, \dotsc, \sqbrk {x_k} }$

Proof:
Define:
:$\map {\phi_g} {y, x_1, \dotsc, x_k} := \map {\phi_f} {0, x_1, \dotsc, x_k, y} \land \forall p < y: \exists q: \paren {q \ne 0 \land \map {\phi_f} {q, x_1, \dotsc, x_k, y} }$
For, by definition of minimization:
:$y = \map g {x_1, \dotsc, x_k}$
{{iff}}
:$\map f {x_1, \dotsc, x_k, y} = 0$
and
:$\map f {x_1, \dotsc, x_k, p}$ is defined and $\ne 0$ for each $p < y$.
That $\phi_g$ is $\Sigma_1$ follows from:
:Conjunction of Existential Quantifier
:Bounded Universal Quantifier Distributes over Conjunction
{{qed}}
Category:Recursive Functions
cowo1wagdti81d7dlawji8rbiunym8b
Theorem: Addition is Arithmetically Definable

Let $f: \N^2 \to \N$ be defined as:
:$\map f {x, y} = x + y$
Then there exists a WFF $\map \phi {z, x, y}$ of $3$ free variables and containing no quantifiers such that:
:$z = \map f {x, y} \iff \N \models \map \phi {\sqbrk z, \sqbrk x, \sqbrk y}$
where $\sqbrk a$ is the unary representation of $a \in \N$.

Proof:
Define:
:$\map \phi {z, x, y} := z = x + y$
Correctness is trivial.
{{qed}}
Category:Natural Number Addition
lamehfpue8qwsjw4b4v78lr8rsi7cyl
Theorem: Multiplication is Arithmetically Definable

Let $f: \N^2 \to \N$ be defined as:
:$\map f {x, y} = x \times y$
Then there exists a WFF $\map \phi {z, x, y}$ of $3$ free variables and containing no quantifiers such that:
:$z = \map f {x, y} \iff \N \models \map \phi {\sqbrk z, \sqbrk x, \sqbrk y}$
where $\sqbrk a$ is the unary representation of $a \in \N$.

Proof:
Define:
:$\map \phi {z, x, y} := z = x \times y$
Correctness is trivial.
{{qed}}
Category:Natural Number Multiplication
fvi8hhh30ljc9u6hn7oi243p1kjf531
Theorem: Remainder is Arithmetically Definable

Let $\operatorname{rem}: \N^2 \to \N$ be defined as:
:$\map \rem {n, m} = \begin{cases}
\text{the remainder when } n \text{ is divided by } m & : m \ne 0 \\
0 & : m = 0
\end{cases}$
where the $\text{remainder}$ is as defined in the Division Theorem:
:If $n = m q + r$, where $0 \le r < m$, then $r$ is the remainder.
Then there exists a $\Sigma_1$ WFF of $3$ free variables:
:$\map \phi {r, n, m}$
such that:
:$r = \map \rem {n, m} \iff \N \models \map \phi {\sqbrk r, \sqbrk n, \sqbrk m}$
where $\sqbrk a$ denotes the unary representation of $a \in \N$.

Proof:
Define:
:$\map \phi {r, n, m} := \paren {m = 0 \land r = 0} \lor \paren {m \ne 0 \land r < m \land \exists q: n = \paren {m \times q} + r}$
Suppose $m = 0$.
Then, only the first case:
:$m = 0 \land r = 0$
can possibly hold.
Therefore, the formula holds {{iff}} $r = 0$, which matches the definition.
Suppose $m \ne 0$.
Then, only the second case:
:$m \ne 0 \land r < m \land \exists q: n = \paren {m \times q} + r$
can possibly hold.
But:
:$r < m \land \exists q: n = \paren {m \times q} + r$
is the definition of $r$.
Therefore, in all cases:
:$r = \map \rem {n, m} \iff \N \models \map \rem {\sqbrk r, \sqbrk n, \sqbrk m}$
{{qed|lemma}}
Finally, that $\phi$ is $\Sigma_1$ follows from:
:Conjunction of Existential Quantifier
:Existential Quantifier Distributes over Disjunction
{{qed}}
nggyafzihtc3b3ygbfaf56apviy2dyj
Theorem: Gödel's Beta Function is Arithmetically Definable

Let Gödel's $\beta$ function $\beta: \N^3 \to \N$ be defined as:
:$\map \beta {x, y, z} = \map \rem {x, 1 + \paren {z + 1} \times y}$
Then there exists a $\Sigma_1$ WFF of $4$ free variables:
:$\map \phi {r, x, y, z}$
such that:
:$r = \map \beta {x, y, z} \iff \N \models \map \phi {\sqbrk r, \sqbrk x, \sqbrk y, \sqbrk z}$
where $\sqbrk a$ denotes the unary representation of $a \in \N$.

Proof:
Follows from:
:Basic Primitive Recursive Functions are Arithmetically Definable
:Addition is Arithmetically Definable
:Multiplication is Arithmetically Definable
:Remainder is Arithmetically Definable
:Substitution of Arithmetically Definable Functions is Arithmetically Definable
{{qed}}
3t1yaqraz24jma4sowyqrblnpw5u1pg
Theorem: Reduction Formula for Primitive of Product of Power with Exponential

Let $n \in \Z_{> 0}$ be a (strictly) positive integer.
Let:
:$I_n := \ds \int x^n e^x \rd x$
Then:
:$I_n = x^n e^x - n I_{n - 1}$
is a reduction formula for $\ds \int x^n e^x \rd x$.

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = x^n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = n x^{n - 1}
      | c = Power Rule for Derivatives
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = e^x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = e^x
      | c = Derivative of Exponential Function
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = I_n
      | r = \int x^n e^x \rd x
      | c = by definition
}}
{{eqn | r = x^n e^x - \int n x^{n - 1} e^x \rd x
      | c = Integration by Parts
}}
{{eqn | r = x^n e^x - n I_{n - 1}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Subset of Cover is Cover of Subset

Let $S$ be a set.
Let $\CC$ be a cover of $S$.
Let $T \subseteq S$.
Let:
:$\CC_T = \set {C \in \CC : C \cap T \ne \O}$
Then $\CC_T$ is a cover of $T$:
:$T \subseteq \bigcup \CC_T$

Proof:
Let $x \in T$.
By definition of a cover:
:$\exists C \in \CC : x \in C$
By definition of set intersection:
:$x \in C \cap T$
Hence:
:$C \in \CC_T$
Since $x$ was arbitrary, it follows that $\CC_T$ is a cover of $T$ by definition and:
:$T \subseteq \bigcup \CC_T$
{{qed}}
Category:Covers
Category:Subsets
o4iohi477mtx4na6qmiwngvgfy4e17n
Theorem: Gödel's Beta Function Lemma

Let $\beta: \N^3 \to \N$ be Gödel's $\beta$ function.
Let $\sequence {x_0, x_1, \dotsc, x_n }$ be a finite sequence of natural numbers.
Then there exist some $a, b \in \N$ such that, for every $i \le n$:
:$\map \beta {a, b, i} = x_i$

Proof:
Let $M = \map \max {n, x_0, x_1, \dotsc, x_n}$.
Define $b = M!$, the factorial of $M$.
Let $\sequence {y_1, y_2, \dotsc, y_{n + 1} }$ be the finite sequence defined by:
:$y_i = 1 + \paren {i \times b}$
As $M \ge n$, by definition:
:$M \ge \paren {n + 1} - 1$
Therefore, by Multiples of Factorial Plus One are Coprime, the $\sequence {y_1, \dotsc, y_{n + 1} }$ are pairwise coprime.
Thus, by the Chinese Remainder Theorem, there exists some $a \in \N$ such that:
{{begin-eqn}}
{{eqn | l = a
      | o = \equiv
      | r = x_0
      | rr = \pmod {y_1}
}}
{{eqn | l = a
      | o = \equiv
      | r = x_1
      | rr = \pmod {y_2}
}}
{{eqn | o = \vdots
}}
{{eqn | l = a
      | o = \equiv
      | r = x_n
      | rr = \pmod {y_{n + 1} }
}}
{{end-eqn}}
But then, for each $0 \le i \le n$:
{{begin-eqn}}
{{eqn | l = y_{i + 1}
      | o = >
      | r = \paren {i + 1} \times b
      | c = Definition of $y_{i + 1}$
}}
{{eqn | o = \ge
      | r = b
      | c = $i \ge 1$
}}
{{eqn | r = M!
      | c = Definition of $b$
}}
{{eqn | o = \ge
      | r = M
}}
{{eqn | o = \ge
      | r = x_i
      | c = Definition of $M$
}}
{{end-eqn}}
Therefore, by the congruence:
:$\map \rem {a, y_{i + 1} } = x_i$
But:
:$y_{i + 1} = 1 + \paren {\paren {i + 1} \times b}$
Thus:
:$\map \rem {a, 1 + \paren {\paren {i + 1} \times b} } = x_i$
But that is the definition of the $\beta$ function.
Hence the result.
{{qed}}
Category:Gödel's Beta Function
huna24twalog1wrubgftt1mi6jq7tbl
Theorem: Primitive Recursion on Arithmetically Definable Function is Arithmetically Definable

Let $f: \N^k \to \N$ and $g: \N^{k+2} \to \N$ be partial functions.
Let $h: \N^{k + 1} \to \N$ be obtained from $f$ and $g$ by primitive recursion.
Let there exist $\Sigma_1$ WFFs:
:$\map {\phi_f} {y, x_1, \dotsc, x_k}$
:$\map {\phi_g} {y, x_1, \dotsc, x_k, n, z}$
of $k + 1$ and $k + 3$ free variables, respectively, such that:
:$y = \map f {x_1, \dotsc, x_k} \iff \N \models \map {\phi_f} {\sqbrk y, \sqbrk {x_1}, \dotsc, \sqbrk {x_k} }$
:$y = \map g {x_1, \dotsc, x_k, n, z} \iff \N \models \map {\phi_g} {\sqbrk y, \sqbrk {x_1}, \dotsc, \sqbrk {x_k}, \sqbrk n, \sqbrk z}$
where $\sqbrk a$ denotes the unary representation of $a \in \N$.
Then there exists a $\Sigma_1$ WFF of $k + 2$ free variables:
:$\map {\phi_h} {y, x_1, \dotsc, x_k, n}$
such that:
:$y = \map h {x_1, \dotsc, x_k, n} \iff \N \models \map {\phi_h} {\sqbrk y, \sqbrk {x_1}, \dotsc, \sqbrk {x_k}, \sqbrk n}$

Proof:
By Gödel's Beta Function is Arithmetically Definable, let:
:$\map {\phi_\beta} {y, a, b, i}$
be a $\Sigma_1$ WFF of $4$ free variables such that:
$y = \map \beta {a, b, i} \iff \N \models \map {\phi_\beta} {\sqbrk y, \sqbrk a, \sqbrk b, \sqbrk i}$
Define $\map {\phi_h} {y, x_1, \dotsc, x_k, n}$ as:
:$\exists a: \exists b: \exists {z_0}: \map {\phi_f} {z_0, x_1, \dotsc, x_k} \land \map {\phi_\beta} {z_0, a, b, 0} \land \map {\phi_\beta} {y, a, b, n} \land \paren {\forall i < n: \exists {z_i}: \exists {z_j}: \map {\phi_\beta} {z_i, a, b, i} \land \map {\phi_\beta} {z_j, a, b, \map s i} \land \map {\phi_g} {z_j, x_1, \dotsc, x_k, i, z_i} }$
To understand this formula, define the finite sequence $\sequence {z_0, \dotsc, z_n}$ defined as:
:$z_i = \map h {x_1, \dotsc, x_k, i}$
By the definition of $h$:
:$z_0 = \map f {x_1, \dotsc, x_k}$
:$z_{i + 1} = \map g {x_1, \dotsc, x_k, i, z_i}$ for all $i < n$
But the formula contains exactly these constraints.
Additionally, as $\phi_\beta$ expresses a function, there is a unique value for the first free variable for which it holds, provided the other variables are held constant.
Then, the formula holds in $\N$ {{iff}} the values for $\map \beta {a, b, i}$ are exactly $\map h {x_1, \dotsc, x_k, i}$.
By Gödel's Beta Function Lemma, there exist $a, b \in \N$ such that:
:$z_i = \map \beta {a, b, i}$
for every $0 \le i \le n$
Therefore, if such $\sequence {z_0, \dotsc, z_n}$ exist, the formula will be true.
Finally, that $\phi_h$ is $\Sigma_1$ follows from:
:Conjunction of Existential Quantifier
:Bounded Universal Quantifier Distributes over Conjunction
{{qed}}
Category:Primitive Recursive Functions
nxqmwhm2lvj7nkikn268jvjjyo02d7d
Theorem: Reduction Formula for Primitive of Product of Power with Power of Quadratic

Let $n \in \Z_{\ge 0}$ and $k \in \Z_{\ge 2}$.
Let:
:$I_{n, k} := \ds \int x^k \paren {x^2 + A x + B}^n \rd x$
Then:
:$I_{n, k} = \dfrac {x^{k - 1} \paren {x^2 + A x + B}^{n + 1} } {k + 2 n + 1} - \dfrac {B \paren {k - 1} } {k + 2 n + 1} I_{n, k - 2} - \dfrac {A \paren {k + n} } {k + 2 n + 1}  I_{n, k - 1}$
is a reduction formula for $\ds \int x^k \paren {x^2 + A x + B}^n \rd x$.

Proof:
Let $h$ be the real function defined as:
:$\forall x \in \R: \map h x = x^2 + A x + B$
Thus we have:
:$I_{n, k} := \ds \int x^k \paren {\map h x}^n \rd x$
Then we have:
{{begin-eqn}}
{{eqn | l = \map {\dfrac \d {\d x} } {x^{k - 1} \paren {\map h x}^{n + 1} }
      | r = x^{k - 1} \map {\dfrac \d {\d x} } {\paren {\map h x}^{n + 1} } + \paren {\map h x}^{n + 1} \dfrac \d {\d x} x^{k - 1}
      | c = Product Rule for Derivatives
}}
{{eqn | r = x^{k - 1} \paren {n + 1} \paren {\map h x}^n \map {\dfrac \d {\d x} } {\map h x} + \paren {\map h x}^{n + 1} \paren {k - 1} x^{k - 2}
      | c = Power Rule for Derivatives, Chain Rule for Derivatives
}}
{{eqn | r = x^{k - 1} \paren {n + 1} \paren {\map h x}^n \paren {2 x + A} + \paren {\map h x}^{n + 1} \paren {k - 1} x^{k - 2}
      | c = Power Rule for Derivatives
}}
{{eqn | r = \paren {\map h x}^n \paren {x^{k - 1} \paren {n + 1} \paren {2 x + A} + \map h x \paren {k - 1} x^{k - 2} }
      | c = extracting $\paren {\map h x}^n$
}}
{{eqn | r = \paren {\map h x}^n \paren {2 \paren {n + 1} x^k + A \paren {n + 1} x^{k - 1} + \paren {x^2 + A x + B} \paren {k - 1} x^{k - 2} }
      | c = substituting for $\map h x$, some simplification
}}
{{eqn | r = \paren {\map h x}^n \paren {\paren {2 \paren {n + 1} + \paren {k - 1} } x^k + A \paren {\paren {n + 1} + \paren {k - 1} } x^{k - 1} + B \paren {k - 1} x^{k - 2} }
      | c = gathering powers of $x$
}}
{{eqn | r = \paren {\map h x}^n \paren {\paren {k + 2 n + 1} x^k + A \paren {k + n} x^{k - 1} + B \paren {k - 1} x^{k - 2} }
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = x^{k - 1} \paren {\map h x}^{n + 1}
      | r = \int \paren {\map h x}^n \paren {\paren {k + 2 n + 1} x^k + A \paren {k + n} x^{k - 1} + B \paren {k - 1} x^{k - 2} } \rd x
      | c = integrating both sides {{WRT|Integration}} $x$
}}
{{eqn | r = \paren {k + 2 n + 1} \int x^k \paren {\map h x}^n \rd x + A \paren {k + n} \int x^{k - 1} \paren {\map h x}^n \rd x + B \paren {k - 1} \int x^{k - 2} \paren {\map h x}^n \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | ll= \leadsto
      | l = x^{k - 1} \paren {x^2 + A x + B}^{n + 1}
      | r = \paren {k + 2 n + 1} I_{n, k} + A \paren {k + n} I_{n, k - 1} + B \paren {k - 1} I_{n, k - 2}
      | c = Definition of $I_{n, k}$ and so on, and substituting for $\map h x$
}}
{{eqn | ll= \leadsto
      | l = I_{n, k}
      | r = \dfrac {x^{k - 1} \paren {x^2 + A x + B}^{n + 1} } {k + 2 n + 1} - \dfrac {B \paren {k - 1} } {k + 2 n + 1} I_{n, k - 2} - \dfrac {A \paren {k + n} } {k + 2 n + 1}  I_{n, k - 1}
      | c = rearrangement
}}
{{end-eqn}}
{{qed}}
Theorem: Characterization of Paracompactness in T3 Space/Lemma 11

:$\forall A \in \AA, V^* \in \VV^* : A \cap V^* \ne \O \implies A \cap V \ne \O$

Proof:
We prove the contrapositive statement:
:$\forall A \in \AA, V \in \VV^* : A \cap V = \O \implies A \cap V^* = \O$
Let $B \in \AA, V^* \in \VV^* : B \cap V = \O$.
Hence:
:$B \in \set{A \in \AA : A \cap V = \O }$
From Set is Subset of Union:
:$B \subseteq \ds \bigcup \set{A \in \AA : A \cap V = \O }$
We have:
{{begin-eqn}}
{{eqn | l = V^*
      | r = X \setminus \bigcup \set {A \in \AA : A \cap V = \O }
      | c = definition of $V^*$
}}
{{eqn | o = \subseteq
      | r = X \setminus B
      | c = Set Difference with Subset is Superset of Set Difference
}}
{{end-eqn}}
From Subset of Set Difference iff Disjoint Set:
:$V^* \cap B = \O$
Since $B$ and $V^*$ were arbitrary:
:$\forall A \in \AA, V^* \in \VV^* : A \cap V = \O \implies A \cap V^* = \O$
The result follows from Rule of Transposition.
{{qed}}
Category:Characterization of Paracompactness in T3 Space
blcs3xu2sbmkz0ryk07j6jg84yd13bk
Theorem: Characterization of Paracompactness in T3 Space/Statement 1 implies Statement 6

Let $T = \struct {X, \tau}$ be a topological space.
If $T$ is paracompact then:
:every open cover of $T$ has an open $\sigma$-locally finite refinement

Proof:
{{Recall|Paracompact Space}}
{{:Definition:Paracompact Space}}
From Locally Finite Set of Subsets is Sigma-Locally Finite Set of Subsets:
:every open cover of $T$ has an open $\sigma$-locally finite refinement.
Theorem: Discrete Set of Subsets is Locally Finite

Let $T = \struct {S, \tau}$ be a topological space.
Let $\FF$ be a discrete set of subsets of $S$.
Then $\FF$ is a locally finite set of subsets of $S$.

Proof:
{{Recall|Discrete Set of Subsets|discrete set of subsets}}
{{:Definition:Discrete Set of Subsets}}
{{Recall|Locally Finite Set of Subsets|locally finite set of subsets}}
{{:Definition:Locally Finite Set of Subsets}}
The result follows immediately.
{{qed}}
Category:Discrete Sets of Subsets
Category:Locally Finite Sets of Subsets
igugszbpva90ui1ot1333wp03rzepdl
Theorem: Sigma-Discrete Set of Subsets is Sigma-Locally Finite

Let $T = \struct {S, \tau}$ be a topological space.
Let $\FF$ be a $\sigma$-discrete set of subsets of $S$.
Then $\FF$ is a $\sigma$-locally finite set of subsets of $S$.

Proof:
{{Recall|Sigma-Discrete Set of Subsets|$\sigma$-discrete set of subsets}}
{{:Definition:Sigma-Discrete Set of Subsets}}
{{Recall|Sigma-Locally Finite Set of Subsets|$\sigma$-locally finite set of subsets}}
{{:Definition:Sigma-Locally Finite Set of Subsets}}
The result follows immediately from Discrete Set of Subsets is Locally Finite.
{{qed}}
Category:Sigma-Discrete Sets of Subsets
Category:Sigma-Locally Finite Sets of Subsets
e74rf0eavwi5qt3fbhffnq1bf4q1wdv
Theorem: Recursive Function is Arithmetically Definable

Let $f: \N^k \to \N$ be a recursive function.
Then there exists a $\Sigma_1$ WFF of $k + 1$ free variables:
:$\map \phi {y, x_1, x_2, \dotsc, x_k}$
such that:
:$y = \map f {x_1, x_2, \dotsc, x_k} \iff \N \models \map \phi {\sqbrk y, \sqbrk {x_1}, \sqbrk {x_2}, \dotsc, \sqbrk {x_k} }$
where $\sqbrk a$ denotes the unary representation of $a \in \N$.

Proof:
By definition of recursive function:
:$f$ can be obtained from basic primitive recursive functions using the operations of:
::substitution
::primitive recursion, and 
::minimization on a function
:a finite number of times.
The existence of $\phi$ follows from:
:Basic Primitive Recursive Functions are Arithmetically Definable
:Substitution of Arithmetically Definable Functions is Arithmetically Definable
:Primitive Recursion on Arithmetically Definable Function is Arithmetically Definable
:Minimization of Arithmetically Definable Function is Arithmetically Definable
{{qed}}
Category:Recursive Functions
mhx5o8zsnhza6r9qwt7edhscpw9ewft
Theorem: Refinement of a Refinement is Refinement of Cover

Let $S$ be a set.
Let $\UU = \set {U_\alpha}$, $\VV = \set {V_\beta}$ and $\WW = \set {W_\gamma}$ be covers of $S$.
Let $\VV$ be a refinement of $\UU$.
Let $\WW$ be a refinement of $\VV$.
Then:
:$\WW$ is a refinement of $\UU$

Proof:
Let $W \in \WW$.
By definition of refinement:
:$\exists V \in \VV : W \subseteq V$
Similarly:
:$\exists U \in \UU : V \subseteq U$
From Subset Relation is Transitive:
:$W \subseteq U$
Since $W$ was arbitrary:
:$\forall W \in \WW : \exists U \in \UU : W \subseteq U$
It follows that $\WW$ is a refinement of $\UU$ by definition.
{{qed}}
Category:Covers
ior7avbmiqjl3pyuw9iepmyr8wbwdae
Theorem: Sigma-Locally Finite Cover has Locally Finite Refinement/Lemma 1

:$\BB$ is a cover of $X$

Proof:
Let $x \in X$.
By definition of cover of set:
:$\exists S \in \SS : x \in S$
By definition of union:
:$\exists n \in \N : S \in \SS_n$
From Set is Subset of Union:
:$S \subseteq B_n$
By definition of subset:
:$x \in B_n$
It follows by definition, $\BB$ is a cover of $X$.
{{qed}}
Category:Sigma-Locally Finite Cover has Locally Finite Refinement
cmshwxm43hgd1zfe166e8qn6pstkbx8
Theorem: Sigma-Locally Finite Cover has Locally Finite Refinement/Lemma 2

:$\CC$ is a locally finite refinement of $\BB$

Proof:
==== Lemma 1 ====
{{:Sigma-Locally Finite Cover has Locally Finite Refinement/Lemma 1}}{{qed|lemma}}
Theorem: Sigma-Locally Finite Cover and Countable Locally Finite Cover have Common Locally Finite Refinement

Let $T = \struct {X, \tau}$ be a topological space.
Let:
:$\SS = \ds \bigcup_{n \mathop = 0}^\infty \SS_n$ be a $\sigma$-locally finite cover of $X$
where each $\SS_n$ is locally finite for all $n \in \N$.
Let $\CC = \set {C_n : n \in \N}$ be a countable locally finite cover of $X$.
Then:
:there exists a common locally finite refinement $\AA$ of both $\SS$ and $\CC$

Proof:
Let:
:$\AA = \set {C_n \cap S : n \in \N, S \in \SS_n}$
Theorem: Sigma-Locally Finite Cover has Locally Finite Refinement

Let $T = \struct {X, \tau}$ be a topological space.
Let $\SS  = \ds \bigcup_{n \mathop = 0}^\infty \SS_n$ be a $\sigma$-locally finite cover of $X$, where each $\SS_n$ is locally finite for all $n \in \N$.
Then:
:there exists a locally finite refinement $\AA$ of $\SS$.

Proof:
For each $n \in \N$, let:
:$B_n = \bigcup \SS_n$
Let:
:$\BB = \set {B_n : n \in \N}$
Theorem: Nonexistence of Continuous Linear Transformations over Finite Dimensional Vector Space whose Commutator equals Identity

Let $\struct {X, \norm {\, \cdot \,}}$ be a normed vector space.
Let $\map {CL} X := \map {CL} {X, X}$ be the space of continuous linear transformations.
Let $A, B \in \map {CL} {X, X}$ be continuous linear transformations.
Let $I$ be the identity operator.
Then there is no $A, B$ such that $A \circ B - B \circ A = I$

Proof:
{{AimForCont}} there is $A, B$ such that $A \circ B - B \circ A = I$.
Theorem: Locally Finite Set of Subsets is Sigma-Locally Finite Set of Subsets

Let $T = \struct {S, \tau}$ be a topological space.
Let $\AA$ be a locally finite set of subsets.
Then:
:$\AA$ is a $\sigma$-locally finite set of subsets.

Proof:
For each $n \in \N$, let:
:$\AA_n = \AA$
Then:
:$\AA = \ds \bigcup_{n \mathop \in \N} \AA_n$
The result follows.
{{qed}}
Category:Locally Finite Sets of Subsets
Category:Sigma-Locally Finite Sets of Subsets
lrpmdhh948t6ste5rn1zsauijnk3xa9