reformulate proof of lemma

Author: ScriptRaccoon

databases/catdat/data/009_lemmas/001_lemmas.sql

@@ -181,8 +181,10 @@ INSERT INTO lemmas (
 (
     'cofiltered-limit-of-non-empty-compact',
     'Cofiltered limits of non-empty compact Hausdorff spaces are non-empty',
-    'Let $\I$ be a cofiltered category, and let $X : \I \to \CompHaus$ be a cofiltered diagram in which $X_i$ is non-empty for each $i\in \I$. Then $\lim_i X_i$ is also non-empty.',
-    'Consider the product space $\prod_{i\in \I} X_i$. Now for each morphism $f : i \to j$ in $\I$, define the subset $E_f := \{ x \in \prod_{i\in\I} X_i \mid X_f(x_i) = x_j \}$. Then each $E_f$ is a closed subset.<br>
-    Now consider a finite collection $\{ E_{f_a} \mid a \in [n] \}$, where each $f_a : i_a \to j_a$. Then the diagram with objects $\{ i_a \} \cup \{ j_a \}$ and morphisms $\{ f_a \}$ has a cone with initial vertex $k \in \I$ and morphisms $g_i$ for each $i \in \{ i_a \} \cup \{ j_a \}$. Now choose $y \in X_k$, and define $x \in \prod_{i\in \I} X_i$ such that $x_i = g_i(y)$ if $i \in \{ i_a \} \cup \{ j_a \}$, with arbitrary choices of $x_i \in X_i$ if $i \notin \{ i_a \} \cup \{ j_a \}$. We then see that $x \in \bigcap_{a=1}^n E_{f_a}$.<br>
-    We have thus shown that the collection $\{ E_f \}$ has the finite intersection property. Since $\prod_{i\in \I} X_i$ is compact, that implies that the intersection of all $E_f$ is non-empty. But that intersection is precisely $\lim_{i\in \I} X_i$.'
+    'Let $\I$ be a cofiltered category, and let $X : \I \to \CompHaus$ be a cofiltered diagram in which $X_i$ is non-empty for each $i \in \I$. Then its limit $\lim_{i \in \I} X_i$ is also non-empty.',
+    'Consider the product space $\prod_{i \in \I} X_i$. Now for each morphism $f : i \to j$ in $\I$, define the subset
+    $$\textstyle E_f := \bigl\{ x \in \prod_{i \in \I} X_i \mid X_f(x_i) = x_j \bigr\}.$$
+    Then each $E_f$ is a closed subset.<br>
+    Next, we prove that the collection $\{ E_f : f \in \Mor(\I) \}$ has the finite intersection property, i.e. that $\bigcap_{f \in F} E_f$ is non-empty for every finite set $F \subseteq \Mor(\I)$. For $f \in F$ we write $f : i_f \to j_f$. Then the diagram with objects $J := \{ i_f : f \in F \} \cup \{ j_f : f \in F\}$ and morphisms $\{ f : f \in F \}$ has a cone with vertex $k \in \I$ and morphisms $g_i : k \to i$ for each $i \in J$. Now choose $y \in X_k$, and define $x \in \prod_{i \in \I} X_i$ such that $x_i = X_{g_i}(y)$ if $i \in J$, with arbitrary choices of $x_i \in X_i$ for all other $i$. We then see that $x \in \bigcap_{f \in F} E_f$, which finishes the proof of the claim.<br>
+    Since $\prod_{i \in \I} X_i$ is compact, that implies that the intersection of all $E_f$ is non-empty. But that intersection is precisely $\lim_{i \in \I} X_i$.'
 );