summaryrefslogtreecommitdiff
path: root/library/topology
diff options
context:
space:
mode:
Diffstat (limited to 'library/topology')
-rw-r--r--library/topology/basis.tex20
1 files changed, 11 insertions, 9 deletions
diff --git a/library/topology/basis.tex b/library/topology/basis.tex
index 61a358f..6fc07d3 100644
--- a/library/topology/basis.tex
+++ b/library/topology/basis.tex
@@ -79,36 +79,38 @@
\begin{lemma}\label{inters_in_genopens}
Assume $B$ is a topological basis for $X$.
- %For all $A, C$
- If $A\in \genOpens{B}{X}$ and $C\in \genOpens{B}{X}$ then $(A\inter C) \in \genOpens{B}{X}$.
+ Suppose $A, C\in \genOpens{B}{X}$.
+
+ Then $(A\inter C) \in \genOpens{B}{X}$.
\end{lemma}
\begin{proof}
Show $(A \inter C) \in \pow{X}$.
\begin{subproof}
- $(A \inter C) \subseteq X$ by assumption.
+ Omitted.
\end{subproof}
- Therefore for all $A, C \in \genOpens{B}{X}$ we have $(A \inter C) \in \pow{X}$.
Show for all $x\in (A\inter C)$ there exists $W \in B$
such that $x\in W$ and $W \subseteq (A\inter C)$.
\begin{subproof}
Fix $x \in (A\inter C)$.
- There exist $V' \in B$ such that $x \in V'$ and $V' \subseteq A$ by assumption. %TODO: Warum muss hier by assumtion hin?
- There exist $V'' \in B$ such that $x \in V''$ and $V'' \subseteq C$ by assumption.
- There exist $W \in B$ such that $x \in W$ and $W \subseteq v'$ and $W \subseteq V''$ by assumption.
+ $x \in A,C$.
+ There exist $V' \in B$ such that $x \in V'$ and $V' \subseteq A$ by \cref{genopens}.
+ There exist $V'' \in B$ such that $x \in V''$ and $V'' \subseteq C$ by \cref{genopens}.
+ $x \in (V' \inter V'')$.
+ There exist $W \in B$ such that $x \in W$ and $W \subseteq V'$ and $W \subseteq V''$.
Show $W \subseteq (A\inter C)$.
\begin{subproof}
%$W \subseteq v'$ and $W \subseteq V''$.
- For all $y \in W$ we have $y \in V'$ and $y \in V''$ by assumption.
+ For all $y \in W$ we have $y \in V'$ and $y \in V''$.
\end{subproof}
\end{subproof}
%Therefore for all $A, C, x$ such that $A \in \genOpens{B}{X}$ and $C \in \genOpens{B}{X}$ and $x \in (A \inter C)$ we have there exists $W \in B$
%such that $x\in W$ and $W \subseteq (A\inter C)$.
- $(A\inter C) \in \genOpens{B}{X}$ by assumption.
+ $(A\inter C) \in \genOpens{B}{X}$.
\end{proof}