I'm reading these notes on the proof of Tychonoff's theorem using nets. I'd appreciate a proof verification, and an alternative proof strategy for the second lemma.
Directed set: A directed set is a partial order $J$ which has "weak joins". That is, for every $a, b \in J$, there exists (not necessarily unique) a $u \in J$ such that $a \leq u$ and $b \leq u$.
Nets: Let $X$ be a topological space. A net is a function $f$ from a directed set $J$ into $X$. We usually write this as $(x_j)$.
Net eventually in a subset $A$: A net $(x_j)$ is eventually in a subset $A$ iff there exists an $i \in J$ such that for all $j$, $j \geq i \implies x_j \in A$.
Net frequently in a subset $A$: A net $(x_j)$ is frequently in a subset $A$ if for all $j \in J$, there exists a $k \in J$ such that $j \leq k$ and $x_k \in A$.
Lemma 1: Eventually not in $X\setminus A$ implies frequently in $A$:
Let the net be $(x_i)$ with index set $J$. Since the net is eventually not in $X\setminus A$, there is an index $e \in J$ (for eventually) such that for all $i \in J, e \leq i \implies x_i \not \in X\setminus A$, or or $x_i \in A$. Now, pick some index $f$ (For frequently) at which we need to establish that the net is frequently in $A$. Since the net is directed, there is an upper bound of $f$ and $e$, say $u$ (for upper bound) such that $e \leq u$, $f \leq u$. By the definition of eventually not being in $X\setminus A$, $e \leq u \implies x_u \in A$. So, we have an index $u$: $f \leq u \land x_u \in A$. QED.
Lemma 2: Frequently in $A$ implies eventually not in $X\setminus A$:
Let the net be $(x_j)$ with index set $J$. Since the net is frequently in $A$, for each $i \in J$, we have an index $f_i \in J$ (for frequently) such that $i \leq f_i$ and $x_{f_i} \in A$. We need to show that there exists some index $e \in J$ (for eventually) such that for all $j \in J$ such that $e \leq j$, we have that $x_j \in A$. Intuitively, we take the index $e$ to be upper bound of all indeces $\{ f_i : i \in J \}$. However, formally, we can't do this. So how do we prove it?
Here's one shot: Assume that the net is both frequently in $A$ (given) and for contradiction, that is not eventually not in $X\setminus A$. That is, it is eventually in $X\setminus A$. This means that there is an index $e$ such that $e \leq i \implies x_i \in X\setminus A$. This means $e \leq i \implies x_i \not \in A$. Since we assumed that we are frequently in $A$, there is an index $f_e$ such that $e \leq f_e \land x_{f_e} \in A$. This contradicts our assumption that $e \leq i \implies x_i \not \in A$. Hence, contradiction. QED.
- Is the proof correct?
- Is there a non-proof-by-contradiction for the second lemma?
I will first point out that the result mentioned is phrased slightly differently, namely that a net is not frequently in $A$ iff it is eventually in $X\setminus A.$ This is an important distinction. You're trying to prove instead that a net is "eventually not in $X\setminus A$" iff it is frequently in $A.$ However, the bit in quotes has not been defined. You seem to be thinking of it as meaning "eventually in $A,$" and indeed, if a net is eventually in $A,$ then it is frequently in $A,$ but the converse need not hold. For a simple example, consider $J=\Bbb N,$ $X=\Bbb R,$ $x_j:=(-1)^j,$ and take $A=\{1\}.$ Readily $(x_j)$ is frequently in $A,$ but it is not "eventually not in $X\setminus A$." This is exactly why you were stymied in your attempt to prove Lemma 2 by your first approach.
As for your approach by contradiction, you've made an error in your negation. The negation of "eventually not in $X\setminus A$" (or of "eventually in $A$") is not the same as "eventually in $X\setminus A$." Rather, it turns out to be the same as "frequently in $X\setminus A$." Thus, while you certainly arrived at a contradiction, the proof attempt is not valid. No contradiction need arise from the assumption that a net is both frequently in $A$ and frequently in $X\setminus A,$ as my example above shows.
One could equivalently prove instead that a net $(x_j)_{j\in J}$ is frequently in $A$ iff it is not eventually in $X\setminus A$, though. But what does the latter mean? Well, it is the negation of being eventually in $X\setminus A.$ Let's consider the definitions formally, so we can see how to negate it. Here is the definition of being eventually in $A$: $$\exists i\in J:\forall j\in J,(j\ge i\implies x_j\in X\setminus A).$$ Equivalently, we could express this as $$\exists i\in J:\forall j\in J,(x_j\in X\setminus A)\vee\neg(j\ge i).$$ At this point, we can negate it relatively straightforwardly, by noting that the following are equivalent: $$\neg\bigl[\exists i\in J:\forall j\in J,(x_j\in X\setminus A)\vee\neg(j\ge i)\bigr]\\\forall i\in J,\neg\bigl[\forall j\in J,(x_j\in X\setminus A)\vee\neg(j\ge i)\bigr]\\\forall i\in J,\exists j\in J:\neg\bigl[(x_j\in X\setminus A)\vee\neg(j\ge i)\bigr]\\\forall i\in J,\exists j\in J:\neg(x_j\in X\setminus A)\wedge\neg\bigl[\neg(j\ge i)\bigr]\\\forall i\in J,\exists j\in J:(x_j\notin X\setminus A)\wedge(j\ge i)\\\forall i\in J,\exists j\in J:(x_j\in A)\wedge(j\ge i)\\\forall i\in J,\exists j\in J:(x_j\in A)\wedge(i\le j)\\\forall i\in J,\exists j\in J:(i\le j)\wedge(x_j\in A).$$ The final form of the statement is precisely that the net is frequently in $A,$ and we're done.
Hopefully, the work above gives you a sense of how one might approach negating "eventually not in $X\setminus A$," so you can see where your second proof attempt went wrong, but if you have any questions, don't hesitate to let me know!