nyuuzyou/wikis huggingface dataset:
Characterization of Paracompactness in T3 Space/Lemma 14

== Theorem ==
Let $X$ be a set.
Let $X \times X$ denote the cartesian product of $X$ with itself.
Let $\sequence{V_n}_{n \in \N}$ be a sequence of subsets of $X \times X$ containing the diagonal $\Delta_X$ of $X \times X$:
:$\forall n \in \N_{> 0}$ the composite relation $V_n \circ V_n$ is a subset of $V_{n - 1}$, that is, $V_n \circ V_n \subseteq V_{n - 1}$
For all $n \in \N_{> 0}$, let:
:$U_n = V_n \circ V_{n - 1}, \circ \cdots \circ V_1$
Then:
:$\forall n \in \N_{>0}: U_n \subseteq V_0$
== Proof ==
=== Proof: $V_n \subseteq V_{n - 1}$ ===
We have:
=== Proof: $U_n \subseteq V_{n - 1} \circ U_{n - 1}$ ===
We have:
=== Proof: $V_n \circ U_n \subseteq V_0$ ===
Proceeds by induction on $n$.
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$V_n \circ U_n \subseteq V_0$
==== Basis for the Induction ====
$\map P 1$ is the case:
and $\map P 1$ is seen to hold.
This is our basis for the induction.
==== Induction Hypothesis ====
Now we need to show that, if $\map P n$ is true, where $n > 0$, then it logically follows that $\map P {n + 1}$ is true.
So this is our induction hypothesis:
:$V_n \circ U_n \subseteq V_0$
Then we need to show:
:$V_{n + 1} \circ U_{n + 1} \subseteq V_0$
==== Induction Step ====
This is our induction step:
So $\map P n \implies \map P {n + 1}$ and by the Principle of Mathematical Induction:
:$(3):\quad\forall n \in \N_{> 0} : V_n \circ U_n \subseteq V_0$
=== Proof: $U_n \subseteq V_0$ ===
We have:
Category:Characterization of Paracompactness in T3 Space
Characterization of Paracompactness in T3 Space/Lemma 15

== Theorem ==
Let $X$ be a set.
Let $X \times X$ denote the cartesian product of $X$ with itself.
Let $\sequence {V_n}_{n \in \N}$ be a sequence of subsets of $X \times X$ containing the diagonal $\Delta_X$ of $X \times X$:
:$\forall n \in \N_{> 0}$ the composite relation $V_n \circ V_n$ is a subset of $V_{n - 1}$, that is, $V_n \circ V_n \subseteq V_{n - 1}$
For all $n \in \N_{> 0}$, let:
:$U_n = V_n \circ V_{n - 1}, \circ \cdots \circ V_1$
Then:
:$\forall n \in \N_{>0}: \set{\map {U_n} x : x \in X}$ refines $\set{\map {V_0} x : x \in X}$
== Proof ==
From Composite of Reflexive Relations is Reflexive:
:$\forall n \in \N_{>0} : U_n$ is reflexive.
From Set of Images of Reflexive Relation is Cover of Set:
:$\set{\map {V_0} x : x \in X}$ is a cover of $X$.
and
:$\forall n \in \N_{>0} : \set{\map {U_n} x : x \in X}$ is a cover of $X$.
==== Lemma 14 ====
Let $n \in \N_{>0}$.
Let $x \in X$.
From Corollary to Image under Subset of Relation is Subset of Image under Relation:
:$\map {U_n} x \subseteq \map {V_0} x$
Since $n$ and $x$ were arbitrary, we have:
:$\forall n \in \N_{>0}, x \in X : \map {U_n} x \subseteq \map {V_0} x$
By definition of refinement:
:$\forall n \in \N : \set{\map {U_n} x : x \in X}$ refines $\set{\map {V_0} x : x \in X}$
Category:Characterization of Paracompactness in T3 Space
Characterization of Paracompactness in T3 Space/Lemma 16

== Theorem ==
Let $X$ be a set with well-ordering $\preccurlyeq$ on $X$.
Let $X \times X$ denote the cartesian product of $X$ with itself.
Let $\sequence{V_n}_{n \in \N}$ be a sequence of subsets of $X \times X$ containing the diagonal $\Delta_X$ of $X \times X$:
:$\forall n \in \N_{> 0}, V_n$ is symmetric as a relation on $X \times X$
:$\forall n \in \N_{> 0}$, the composite relation $V_n \circ V_n$ is a subset of $V_{n - 1}$, that is, $V_n \circ V_n \subseteq V_{n - 1}$
For all $n \in \N_{> 0}$, let:
:$U_n = V_n \circ V_{n - 1}, \circ \cdots \circ V_1$
For each $n \in \N_{> 0}, x \in X$, let:
:$\map {A_n} x = \map {U_n} x \setminus \ds \bigcup_{y \preccurlyeq x, y \ne x} \map {U_{n + 1}} y$
Then:
:$\forall n \in \N_{> 0}, \forall y, z \in X : y \ne z \leadsto \map {A_n} z \cap V_{n+1} \sqbrk {\map {A_n} y} = \O$
== Proof ==
Let $n \in \N_{> 0}$.
Let $y, z \in X : y \ne z$.
=== Case 1: $y \preccurlyeq z$ ===
We have:
From Set Intersection Preserves Subsets:
From Set Difference Intersection with Second Set is Empty Set:
From Intersection is Empty Implies Intersection of Subsets is Empty:
=== Case 2: $z \preccurlyeq y$ ===
Applying the same argument used in Case 1 with $y$ and $z$ swapped around:
:$(1):\quad\map {A_n} y \cap V_{n + 1} \sqbrk {\map {A_n} z} = \O$
We have:
Hence:
:$V_{n + 1} \sqbrk{\map {A_n} z \cap V_{n + 1} \sqbrk {\map {A_n} y} } = \O$
From Image under Left-Total Relation is Empty iff Subset is Empty:
:$\map {A_n} z \cap V_{n + 1} \sqbrk {\map {A_n} y} = \O$
In either case, we have:
:$\map {A_n} z \cap V_{n+1} \sqbrk {\map {A_n} y} = \O$
Since $n$, $y$ and $z$ were arbitrary, we have:
:$\forall n \in \N_{> 0}, \forall y, z \in X : y \ne z \leadsto \map {A_n} z \cap V_{n+1} \sqbrk {\map {A_n} y} = \O$
Category:Characterization of Paracompactness in T3 Space
Characterization of Paracompactness in T3 Space/Lemma 17

== Theorem ==
Let $X$ be a set with well-ordering $\preccurlyeq$ on $X$.
Let $X \times X$ denote the cartesian product of $X$ with itself.
Let $\sequence{V_n}_{n \in \N}$ be a sequence of subsets of $X \times X$ containing the diagonal $\Delta_X$ of $X \times X$:
:$\forall n \in \N_{> 0}, V_n$ is symmetric as a relation on $X \times X$
:$\forall n \in \N_{> 0}$, the composite relation $V_n \circ V_n$ is a subset of $V_{n - 1}$, that is, $V_n \circ V_n \subseteq V_{n - 1}$
For all $n \in \N_{> 0}$, let:
:$U_n = V_n \circ V_{n - 1}, \circ \cdots \circ V_1$
For each $n \in \N_{> 0}, x \in X$, let:
:$\map {A_n} x = \map {U_n} x \setminus \ds \bigcup_{y \preccurlyeq x, y \ne x} \map {U_{n + 1}} y$
For each $n \in \N_{> 0}$, let:
:$\AA_n = \set{\map {A_n} x : x \in X}$
Then:
:$\forall n \in \N_{> 0} : \AA_n$ is a discrete set of subsets.
== Proof ==
=== Lemma 16 ===
Let $n \in \N_{> 0}$.
Let $x \in X$.
===== Case: $\forall y : \map {V_{n+1} } x \cap \map {A_n} y = \O$ =====
For all $y \in X$, let:
:$\map {V_{n+1} } x \cap \map {A_n} y = \O$
From Image of Point under Neighborhood of Diagonal is Neighborhood of Point:
:$\map {V_{n+1} } x$ is a neighborhood of $x$ in $T$ that intersects no element of $\AA_n$
===== Case: $\exists y : \map {V_{n+1} } x \cap \map {A_n} y \ne \O$ =====
Let $y \in X$:
:$\map {V_{n+1} } x \cap \map {A_n} y \ne \O$
From Image under Left-Total Relation is Empty iff Subset is Empty:
:$V_{n + 1} \sqbrk {\map {V_{n+1} } x \cap \map {A_n} y} \ne \O$
We have:
From Subset of Empty Set:
:$\set x \cap V_{n + 1} \sqbrk {\map {A_n} y} \ne \O$
Hence:
:$\set x \subseteq V_{n + 1} \sqbrk {\map {A_n} y}$
We have:
From Image of Subset under Neighborhood of Diagonal is Neighborhood of Subset:
:$V_{n + 1} \sqbrk {\map {A_n} y}$ is a neighborhood of $\map {A_n} y$
From Set is Neighborhood of Subset iff Neighborhood of all Points of Subset:
:$V_{n + 1} \sqbrk {\map {A_n} y}$ is a neighborhood of $x$
From Lemma 16:
:$\forall z \in X : y \ne z \leadsto \map {A_n} z \cap V_{n+1} \sqbrk {\map {A_n} y} = \O$
Hence $V_{n+1} \sqbrk {\map {A_n} y}$ is a neighborhood of $x$ in $T$ that intersects at most one element of $\AA_n$.
In either case:
:there exists a neighborhood of $x$ in $T$ that intersects at most one element of $\AA_n$.
Since $x$ was arbitrary:
:For all $x \in X$ there exists a neighborhood of $x$ in $T$ that intersects at most one element of $\AA_n$.
Hence $\AA_n$ is a discrete set of subsets by definition.
Since $n$ was arbitrary:
:$\forall n \in \N_{>0} : \AA_n$ is a discrete set of subsets
Category:Characterization of Paracompactness in T3 Space
Characterization of Paracompactness in T3 Space/Lemma 18

== Theorem ==
Let $X$ be a set with well-ordering $\preccurlyeq$ on $X$.
Let $X \times X$ denote the cartesian product of $X$ with itself.
Let $\sequence{U_n}_{n \in \N}$ be a sequence of subsets of $X \times X$ containing the diagonal $\Delta_X$ of $X \times X$.
For each $n \in \N_{> 0}, x \in X$, let:
:$\map {A_n} x = \map {U_n} x \setminus \ds \bigcup_{y \preccurlyeq x, y \ne x} \map {U_{n + 1}} y$
For each $n \in \N_{> 0}$, let:
:$\AA_n = \set{\map {A_n} x : x \in X}$
Let:
:$\AA = \ds \bigcup_{n \in \N, n \ne 0} \AA_n$
Then:
:$\AA$ is a cover of $X$
== Proof ==
Let $x \in X$.
We have :
:$\forall n \in \N_{>0} : \Delta_X \subseteq U_n$
By definition of image:
:$\forall n \in \N_{>0} : x \in \map {U_n} x$
Let:
:$y = \min \set{z \in X : x \in \ds \bigcup_{n \in N} \map {U_n} z}$
with respect to the well-ordering $\preccurlyeq$.
By choice of $y$
:$\exists n \in \N_{>0}$: $x \in \map {U_n} y$ 
and 
:$\forall z \preccurlyeq y, z \ne y : x \notin \map {U_{n + 1}} z$
By definition of set union:
:$x \notin \ds \bigcup_{z \preccurlyeq y, z \ne y} \map {U_{n + 1}} z$
By definition of set difference
:$x \in \map {U_n} y \setminus \ds \bigcup_{z \preccurlyeq y, z \ne y} \map {U_{n + 1}} z$
That is:
:$x \in \map {A_n} y$
Since $x$ was arbitrary:
:$\forall x \in X : \exists y \in X, n \in \N_{>0} : x \in \map {A_n} y$
Hence $\AA$ is a cover of $X$ by definition.
Category:Characterization of Paracompactness in T3 Space
Characterization of Paracompactness in T3 Space/Lemma 19

== Theorem ==
Let $T = \struct{X, \tau}$ be a topological space.
Let $\BB$ be a discrete set of subsets of $X$.
Let $\UU = \set{ U \in \tau : \size {\set{B \in \BB : U \cap B} } \le 1}$
Then:
:$\UU$ is a open cover of $X$ in $T$.
== Proof ==
Let $s \in X$.
By definition of discrete:
:$\exists U \in \tau : x \in U : \size {\set{B \in \BB : U \cap B} } \le 1$
Hence:
:$U \in \UU$
Since $x$ was arbitrary:
:$\forall x \in X : \exists U \in \UU : x \in U$
It follows that $\UU$ is an open cover of $X$ in $T$ by definition.
Category:Characterization of Paracompactness in T3 Space
Characterization of Paracompactness in T3 Space/Lemma 2

== Theorem ==
Let $T = \struct{X, \tau}$ be a topological space.
Let $\AA$ be a locally finite cover of $T$.
Let $\BB = \set{A^- : A \in \AA}$ be locally finite, where $A^-$ denotes the closure of $A$ in $T$.
Then:
:$\BB$ is a cover of $T$ consisting of closed sets
== Proof ==
Let $x \in X$.
By definition of refinement:
:$\AA$ is a cover of $X$
By definition of cover of set:
:$\exists A \in \AA : x \in A$
From Set is Subset of its Topological Closure:
:$A \subseteq A^-$
By definition of subset:
:$x \in A^-$
By definition of $\BB$:
:$A^- \in \BB$
Since $x$ was arbitrary, $\BB$ is a cover of $T$ by definition.
From Topological Closure is Closed, every element of $\BB$ is closed in $T$
Category:Characterization of Paracompactness in T3 Space
Characterization of Paracompactness in T3 Space/Lemma 20

== Theorem ==
Let $T = \struct{X, \tau}$ be a topological space.
Let every open cover of $T$ be even.
Let $\tau_{X \times X}$ denote the product topology on the cartesian product $X \times X$.
Let $N$ be a neighborhood of the diagonal $\Delta_X$ of $X \times X$ in the product space $\struct {X \times X, \tau_{X \times X} }$.
Then there exists an open neighborhood $W$ of the diagonal $\Delta_X$ in $\struct {X \times X, \tau_{X \times X} }$:
:$W$ is symmetric as a relation on $X \times X$, that is, $W = W^{-1}$
:the composite relation $W \circ W$ is a subset of $N$, that is, $W \circ W \subseteq N$
== Proof ==
Let:
:$\VV = \set{V \in \tau : V \times V \subseteq N}$
From Neighborhood of Diagonal induces Open Cover:
:$\VV$ is an open cover of $T$
We have , $\VV$ is even.
From Characterization of Even Cover, there exists an open neighborhood $R$ of the diagonal $\Delta_X$ in $\struct {X \times X, \tau_{X \times X} }$:
:$\set{\map R x : x \in S}$ is a refinement of $\VV$
where:
:$R$ is seen as a relation on $X \times X$
:$\map R x$ denotes the image of $x$ under $R$.
By definition of refinement of cover:
:$\forall x \in X : \exists V \in \VV : \map R x \subseteq V$
From Cartesian Product of Subsets:
:$\forall x \in X : \exists V \in \VV : \map R x \times \map R x \subseteq V \times V$
From Subset Relation is Transitive:
:$\forall x \in X : \map R x \times \map R x \subseteq N$
Let $W = R \cap R^{-1}$, where $R^{-1}$ is the inverse relation of $R$ on $X \times X$.
From Inverse of Open Set in Product Space is Open in Inverse Product Space:
:$R^{-1}$ is open in $\struct {X \times X, \tau_{X \times X}}$
By :
:$W$ is open in $\struct {X \times X, \tau_{X \times X}}$
From Inverse of Reflexive Relation is Reflexive:
:$R^{-1}$ is reflexive
From Intersection of Reflexive Relations is Reflexive:
:$W$ is reflexive
By definition of reflexive:
:$W$ is an open neighborhood of the diagonal $\Delta_X$.
From Intersection of Relation with Inverse is Symmetric Relation:
:$W$ is a symmetric relation on $X \times X$
We have:
By definition of subset:
:$\forall x \in X : \map W x \times \map W x \subseteq N$
From Composition of Symmetric Relation with Itself is Union of Products of Images:
:$W \circ W = \ds \bigcup_{x \in X} \map W x \times \map W x$
From Union of Subsets is Subset:
:$W \circ W \subseteq N$
== Sources ==
* : Chapter $5$: Compact Spaces: $\S$Paracompactness: Lemma $30$
Category:Characterization of Paracompactness in T3 Space
Characterization of Paracompactness in T3 Space/Lemma 21

== Theorem ==
Let $X$ be a set.
Let $X \times X$ denote the Cartesian product of $X$ with itself.
Let $\BB$ be a set of subsets of $X$.
Let $W \subseteq X \times X$ be symmetric as a relation on $X \times X$.
Then:
:$\forall B \in \BB, x \in X : \map W x \cap W \sqbrk B \ne \O \leadsto \map {W \circ W} x \cap B \ne \O$
where:
:$\map W x$ denotes the image of $x$ under the relation $W$
:$W \sqbrk B$ denotes the image of $B$ under the relation $W$
:$W \circ W$ denotes the composite relation of $W$ with itself
== Proof ==
Let $B \in \BB$.
Let $x \in X$.
Let $y \in \map W x \cap W \sqbrk B$.
By definition of intersection:
:$y \in \map W x$
and
:$y \in W \sqbrk B$
By definition of image of element:
:$\tuple{x, y} \in W$
By definition of symmetric:
:$\tuple{y, x} \in W$
By definition of image of subset:
:$\exists z \in B : \tuple{z, y} \in W$
By definition of composite relation:
:$\exists z \in B : \tuple{z, x} \in W \circ W$
By definition of image of element:
:$z \in \map {W \circ W} x \cap B$
Hence:
:$\map {W \circ W} x \cap B \ne \O$
Since $B$ and $x$ were arbitrary, then:
:$\forall B \in \BB, x \in X : \map W x \cap W \sqbrk B \ne \O \leadsto \map {W \circ W} x \cap B \ne \O$
Category:Characterization of Paracompactness in T3 Space
Characterization of Paracompactness in T3 Space/Lemma 3

== Theorem ==
Let $T = \struct{X, \tau}$ be a topological space.
Let $\UU$ be an open cover of $T$.
Let:
:$\VV = \set{V \in \tau : \exists U \in \UU : V^- \subseteq U}$ be cover of $T$ 
where $V^-$ denotes the closure of $V$ in $T$.
Let $\AA$ be a locally finite refinement of $\VV$.
Let $\BB = \set{A^- : A \in \AA}$ be locally finite.
Then:
:$\BB$ is a refinement of $\UU$
== Proof ==
==== Lemma 2 ====
Let $B \in \BB$.
By definition of $\BB$:
:$\exists A \in \AA : A^- = B$
By definition of refinement:
:$\exists V \in \VV : A \subseteq V$
From Set Closure Preserves Set Inclusion:
:$B = A^- \subseteq V^-$
By definition of $\VV$:
:$\exists U \in \UU : V^- \subseteq U$
From Subset Relation is Transitive:
:$B \subseteq U$
It follows that $\BB$ is a refinement of $\UU$ by definition.
Category:Characterization of Paracompactness in T3 Space
Characterization of Paracompactness in T3 Space/Lemma 4

== Theorem ==
Let $T = \struct{X, \tau}$ be a topological space.
Let $\VV$ be a cover of $T$.
Let $\WW = \set{W \in \tau : \set{V \in \VV : V \cap W \ne \O} \text{ is finite}}$ be an open cover of $T$.
Let $\AA$ be a closed locally finite refinement of $\WW$.
Then:
:$\forall A \in \AA : \set{V \in \VV : V \cap A \ne \O}$ is finite
== Proof ==
Let $A \in \AA$.
By definition of refinement:
:$\exists W \in \WW : A \subseteq W$
From Subsets of Disjoint Sets are Disjoint:
:$\forall V \in \VV : V \cap A \ne \O \leadsto V \cap W \ne \O$
Hence:
:$\set{V \in \VV : V \cap A \ne \O} \subseteq \set{V \in \VV : V \cap W \ne \O}$
We have :
:$\set{V \in \VV : V \cap W \ne \O}$ is finite
From Subset of Finite Set is Finite:
:$\set{V \in \VV : V \cap A \ne \O}$ is finite
Since $A$ was arbitrary, it follows that:
:$\forall A \in \AA : \set{V \in \VV : V \cap A \ne \O}$ is finite
Category:Characterization of Paracompactness in T3 Space
Characterization of Paracompactness in T3 Space/Lemma 5

== Theorem ==
Let $X$ be a set.
Let $\AA$ and $\VV$ be sets of subsets of $X$.
For each $V \in \VV$, let:
:$V^* = X \setminus \ds \bigcup \set{A \in \AA | A \cap V = \O}$
Then:
:$\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:
Category:Characterization of Paracompactness in T3 Space
Characterization of Paracompactness in T3 Space/Lemma 6

== Theorem ==
Let $T = \struct {X, \tau}$ be a topological space.
Let $\UU$ be an open cover of $T$.
Let $\VV$ be a closed locally finite refinement of $\UU$.
For all $x \in X$, let:
:$W_x \in \tau: x \in W_x$ and $\set {V \in \VV : V \cap W \ne \O}$ is finite
Let $\WW = \set {W_x : x \in X}$ be an open cover of $T$.
Let $\AA$ be a closed locally finite refinement of $\WW$.
For each $V \in \VV$, let:
:$V^* = X \setminus \bigcup \set {A \in \AA | A \cap V = \O}$
Let $\VV^* = \set {V^* : V \in \VV}$.
Then:
:$\VV^*$ is an open locally finite cover of $T$
== Proof ==
==== Lemma 4 ====
==== Lemma 11 ====
==== $\VV^*$ is a Set of Open Subsets ====
Let $V^* \in \VV^*$ for some $V \in \VV$.
Let $\AA_V = \set {A \in \AA | A \cap V = \O}$.
By definition of subset:
:$\AA_V \subseteq \AA$
From Subset of Locally Finite Set of Subsets is Locally Finite:
:$\AA_V$ is closed locally finite
From Union of Closed Locally Finite Set of Subsets is Closed:
:$\bigcup \set{A \in \AA | A \cap V = \O}$ is closed in $T$
By definition of closed set:
:$V^* = X \setminus \ds \bigcup \set{A \in \AA | A \cap V = \O} \in \tau$
Since $V^*$ was arbitrary, it follows that:
:$V^* \in \VV^* : V^* \in \tau$ 
==== $\VV^*$ is a Cover ====
Let $x \in X$.
By definition of a cover:
:$\exists V \in \VV : x \in V$
From :
:$V \subseteq V^*$
By definition of subset:
:$x \in V^*$
Since $x$ was arbitrary, it follows that $\VV^*$ is a cover by definition.
==== $\VV^*$ is Locally Finite ====
Let $x \in X$.
By definition of locally finite:
:$\exists U \in \tau : x \in U : \set{A \in \AA : A \cap U \ne \O}$ is finite.
Let $\set{A \in \AA : A \cap U \ne \O} = \set{A_1, A_2, \ldots, A_n}$ for some $n \in \N$.
From Subset of Cover is Cover of Subset:
:$U \subseteq \ds \bigcup \set{A_1, A_2, \ldots, A_n}$
Let:
:$V^* \in \VV^* : V^* \cap U \ne \O$
We have:
Hence:
:$\exists i \in \set{1, 2, \ldots, n} : V^* \cap A_i \ne \O$
From :
:$V \cap A_i \ne \O$
Hence:
:$\set {V^* \in \VV^* : V^* \cap U} \subseteq \set {V^* \in \VV^* : \exists 1 \le i \le n : V \cap A_i \ne \O}$
For each $1 \le i \le n$:
:$\exists W_i \in \WW : A_i \subseteq W_i$
By definition of $\WW$:
:$\forall 1 \le i \le n : \set {V \in \VV : V \cap W_i \ne \O}$ is finite
Hence:
:$\forall 1 \le i \le n : \set {V \in \VV : V \cap A_i \ne \O}$ is finite
From Union of Finite Sets is Finite:
:$\set {V^* \in \VV^* : \exists 1 \le i \le n : V \cap A_i \ne \O}$ is finite
From Subset of Finite Set is Finite:
:$\set {V^* \in \VV^* : V^* \cap U}$ is finite
Since $x$ was arbitrary, it follows that $\VV^*$ is locally finite.
Category:Characterization of Paracompactness in T3 Space
Characterization of Paracompactness in T3 Space/Lemma 7

== Theorem ==
Let $T = \struct{X, \tau}$ be a topological space.
Let $\UU$ be an open cover of $T$.
Let $\VV$ be a closed locally finite refinement of $\UU$.
For all $x \in X$, let:
:$W_x \in \tau: x \in W_x$ and $\set{V \in \VV : V \cap W_x \ne \O}$ be finite
Let $\WW = \set{W_x : x \in X}$ be an open cover of $T$.
Let $\AA$ be a closed locally finite refinement of $\WW$.
For each $V \in \VV$, let:
:$V^* = X \setminus \ds \bigcup \set{A \in \AA | A \cap V = \O}$
Let $\VV^* = \set{V^* : V \in \VV}$.
For each $V \in \VV$, let:
:$U_V \in \UU : V \subseteq U_V$
Let:
:$\UU^* = \set{V^* \cap U_V : V \in \VV}$
Then:
:$\UU^*$ is an open locally finite refinement of $\UU$
== Proof ==
==== Lemma 5 ====
==== Lemma 6 ====
===== Lemma 12 =====
==== $\UU^*$ is an Open Cover of $T$ ====
By :
:$\forall V^* \cap U_V \in \UU^* : V^* \cap U_V \in \tau$
From Set is Subset of Intersection of Supersets:
:$\forall V \in \VV : V \subseteq V^* \cap U_V$
By definition of cover:
:$\forall x \in X : \exists V \in \VV : x \in V$
By definition of subset:
:$\forall x \in X : \exists V \in \VV : x \in V^* \cap U_V$
Hence $\UU^*$ is an open cover of $T$ by definition.
==== $\UU^*$ is a Refinement of $\UU$ ====
From Intersection is Subset:
:$\forall V \in \VV : V^* \cap U_V \subseteq U_V \in \UU$
Hence $\UU^*$ is a refinement of $\UU$.
==== $\UU^*$ is Locally Finite ====
Let $x \in X$.
By definition of locally finite:
:$\exists W \in \tau : x \in W : \set{A \in \AA : A \cap W \ne \O}$ is finite
Let:
:$\set{A \in \VV : A \cap W \ne \O} = \set{A_1, A_2, \ldots, A_k}$ where $k \in \N$
From Subset of Cover is Cover of Subset:
:$W \subseteq \ds \bigcup_{n = 1}^k A_n$
We have:
From Lemma 12:
:$\forall A_i = 1, \ldots , n : \set{U^* \in \UU : U^* \cap A_i \ne \O}$ is finite
From Finite Union of Finite Sets is Finite:
:$\bigcup_{n = 1}^k \set{U^* \in \UU : U^* \cap A_n \ne \O}$ is finite
From Subset of Finite Set is Finite:
:$\set{U^* \in \UU : U^* \cap W \ne \O}$ is finite
Since $x$ was arbitrary:
:$\UU^*$ is locally finite by definition.
Hence:
:$\UU^*$ is an open locally finite refinement of $\UU$ by definition.
Category:Characterization of Paracompactness in T3 Space
Characterization of Paracompactness in T3 Space/Lemma 8

== Theorem ==
Let $T = \struct{X, \tau}$ be a topological space.
Let every open cover of $T$ be even.
Let $\UU$ be an open cover of $T$.
Then:
:there exists a $\sigma$-discrete refinement $\AA$ of $\UU$
== Proof ==
Let $\tau_{X \times X}$ denote the product topology on the cartesian product $X \times X$.
By definition of even cover there exists a neighborhood $V$ of the diagonal $\Delta_X$ of $X \times X$ in the product space $\struct {X \times X, \tau_{X \times X} }$:
:$\set{\map V x : x \in X}$ is a refinement of $\UU$
where:
:$V$ is seen as a relation on $X \times X$
:$\map V x$ denotes the image of $x$ under $V$.
In what follows subsets of $X \times X$ will be treated at times as a relation on $X \times X$.
==== Lemma 13 ====
For all $n \in \N_{> 0}$, let:
:$U_n = V_n \circ V_{n - 1}, \circ \cdots \circ V_1$
Then:
:$\forall n \in \N_{> 0} : U_{n + 1} = V_{n + 1} \circ U_n$
==== Lemma 14 ====
==== Lemma 15 ====
We have :
:$\set{\map {V_0} x : x \in X}$ refines $\UU$
From Refinement of a Refinement is Refinement of Cover: 
:$(1) \quad \forall n \in \N_{>0} : \set{\map {U_n} x : x \in X}$ refines $\UU$
From Zermelo's Well-Ordering Theorem, let:
:$\preccurlyeq$ well-order $X$
For each $n \in \N_{> 0}, x \in X$, let:
:$\map {A_n} x = \map {U_n} x \setminus \ds \bigcup_{y \preccurlyeq x, y \ne x} \map {U_{n + 1}} y$
==== Lemma 16 ====
For each $n \in \N_{> 0}$, let:
:$\AA_n = \set{\map {A_n} x : x \in X}$
==== Lemma 17 ====
Let:
:$\AA = \ds \bigcup_{n \in \N, n \ne 0} \AA_n$
==== Lemma 18 ====
==== $\AA$ Refines $\UU$ ====
Let $x \in X$ and $n \in \N_{>0}$.
From Set Difference is Subset:
:$\map {A_n} x \subseteq \map {U_n} x$
From (1) and definition of refinement:
:$\exists U \in \UU : \map {U_n} x \subseteq U$
From Subset Relation is Transitive:
:$\exists U \in \UU : \map {A_n} x \subseteq U$
Since $x$ and $n$ were arbitrary, then $\AA$ refines $\UU$ by definition.
It follows that $\AA$ is a $\sigma$-discrete refinement of $\UU$ by definition.
Category:Characterization of Paracompactness in T3 Space