View source for Notes:Basis for a topology/Attempt 2

==Overview==
Last time I tried to merge the definitions, which got very confusing! This time I shall treat them as separate things and go from there.
==Definitions==
Here we will use '''GBasis''' for a generated topology (by a basis) and '''TBasis''' for a basis of an existing topology.
===GBasis===
Let {{M|X}} be a [[set]] and {{M|\mathcal{B}\subseteq\mathcal{P}(X)}} be a collection of [[subset of|subsets of]] {{M|X}}. Then we say:
* {{M|\mathcal{B} }} is a '''GBasis''' if it satisfies the following 2 conditions:
*# {{M|\forall x\in X\exists B\in\mathcal{B}[x\in B]}} - every element of {{M|X}} is contained in some GBasis set.
*# {{M|\forall B_1,B_2\in\mathcal{B}\forall x\ B_1\cap B_2\exists B_3\in\mathcal{B}[B_1\cap B_2\ne\emptyset\implies(x\in B_3\subseteq B_1\cap B_2)]}}<ref group="Note">Note that {{M|x\in B_3\subseteq B_1\cap B_2}} is short for:
* {{M|x\in B_3\wedge B_3\subseteq B_1\cap B_2}}</ref><ref group="Note">Note that if {{M|B_1\cap B_2}} is empty (they do not [[intersection|intersect]]) then the [[logical implication]] is true regardless of the RHS of the {{M|\implies}}} sign, so we do not care if we have {{M|x\in B_3\wedge B_3\subseteq B_1\cap B_2}}! Pick any {{M|x\in X}} and aany {{M|B_3\in\mathcal{B} }}!</ref>
Then {{M|\mathcal{B} }} ''induces'' a [[topology]] on {{M|X}}.

Let {{M|\mathcal{J}_\text{Induced} }} denote this topology, then:
* {{M|1=\forall U\in\mathcal{P}(X)\big[U\in\mathcal{J}_\text{Induced}\iff\big(\forall p\in U\exists B\in\mathcal{B}[p\in B\wedge B\subseteq U]\big)\big]}}
===TBasis===
Suppose {{Top.|X|J}} is a [[topological space]] and {{M|\mathcal{B}\subseteq\mathcal{P}(X)}} is some collection of subsets of {{M|X}}. We say:
* {{M|\mathcal{B} }} is a '''TBasis''' if it satisfies both of the following:
*# {{M|\forall B\in\mathcal{B}[B\in\mathcal{J}]}} - all the basis elements are themselves open.
*# {{M|1=\forall U\in\mathcal{J}\exists\{B_\alpha\}_{\alpha\in I}[\bigcup_{\alpha\in I}B_\alpha=U]}}
If we have a '''TBasis''' for a topological space then we may talk about its open sets differently:
* {{M|1=\forall U\in\mathcal{P}(X)\big[U\in\mathcal{J}\iff\big(\forall p\in U\exists B\in\mathcal{B}[p\in B\wedge B\subseteq U]\big)\big]}}
==Facts==
# {{M|\mathcal{B} }} is a '''GBasis''' of {{M|X}} inducing {{M|(X,\mathcal{J}')}} {{M|\implies}} {{M|\mathcal{B} }} is a '''TBasis''' for the {{M|(X,\mathcal{J}')}}
# {{Top.|X|J}} is a [[topological space]] with a '''TBasis''' {{M|\mathcal{B} }} {{M|\implies}} {{M|\mathcal{B} }} is a '''GBasis'''
==Result==
# '''Lemma: ''' {{M|\mathcal{B} }} is a '''TBasis''' of {{M|(X,\mathcal{J})}} {{M|\implies}} {{M|\mathcal{B} }} is a '''GBasis''' (inducing {{M|(X,\mathcal{J}')}}) {{M|\implies}} {{M|\mathcal{B} }} is a '''TBasis''' of {{M|(X,\mathcal{J}')}}
# '''Proposition: ''' {{M|1=\mathcal{J}=\mathcal{J'} }} (using the method of proof of fact 1 part 3 (the bit with the warning - as it isn't needed there))
# '''Theorem: ''' {{M|\mathcal{B} }} is a '''TBasis''' of {{M|(X,\mathcal{J})}} {{M|\implies}} {{M|\mathcal{B} }} is a '''GBasis''' (inducing {{M|(X,\mathcal{J})}}) {{M|\implies}} {{M|\mathcal{B} }} is a '''TBasis''' of {{M|(X,\mathcal{J})}}
# '''Proposition: ''' {{M|\mathcal{B} }} is a '''Tbasis''' of {{M|(X,\mathcal{J})}} {{M|\iff}} {{M|\mathcal{B} }} is a '''GBasis''' inducing {{M|(X,\mathcal{J})}}
==Proof of facts==
# {{M|\mathcal{B} }} is a '''GBasis''' of {{M|X}} inducing {{M|(X,\mathcal{J}')}} {{M|\implies}} {{M|\mathcal{B} }} is a '''TBasis''' for the {{M|(X,\mathcal{J}')}}
#* Let {{M|\mathcal{B} }} be a '''GBasis''', suppose it generates the [[topological space]] {{M|(X,\mathcal{J}')}}, we will show it's also a '''TBasis''' of {{M|(X,\mathcal{J}')}}
#*# {{M|\forall B\in\mathcal{B}[B\in\mathcal{J}']}} must be shown
#*#* Let {{M|B\in\mathcal{B} }} be given.
#*#** Recall {{M|U\in\mathcal{J}'\iff\forall x\in U\exists B'\in\mathcal{B}[x\in B'\wedge B'\subseteq U]}}
#*#** Let {{M|x\in B}} be given. 
#*#*** Choose {{M|1=B':=B}}
#*#**** {{M|x\in B'}} by definition, as {{M|1=x\in B'=B}} and
#*#**** we have {{M|B\subseteq B}}, by the [[implies-subset relation]], {{iff}} {{M|\forall p\in B[p\in B]}} which is trivial.
#*#** Thus {{M|B\in\mathcal{J}'}}
#*#* Since {{M|B\in\mathcal{B} }} was arbitrary we have shown {{M|\forall B\in\mathcal{B}[B\in\mathcal{J}']}}
#*# {{M|1=\forall U\in\mathcal{J}'\exists\{B_\alpha\}_{\alpha\in I}[\bigcup_{\alpha\in I}B_\alpha=U]}} must be shown
#*#* Let {{M|U\in\mathcal{J}'}} be given.
#*#** Then, as {{M|\mathcal{B} }} is a '''GBasis''', by definition of the open sets generated: {{M|\forall x\in X\exists B\in\mathcal{B}[x\in B\wedge B\subseteq U]}}
#*#** Let {{M|p\in U}} be given
#*#*** Define {{M|1=B_p}} to be the {{M|B}} that exists such that {{M|p\in B_p}} and {{M|B_p\subseteq U}}
#*#** We now have an .... thing, like a sequence but arbitrary, {{M|(B_p)_{p\in U} }} or {{M|\{B_p\}_{p\in U} }} - I need to come down on a notation for this - such that:
#*#*** {{M|\forall B_p\in(B_p)_{p\in U}[p\in B_p\wedge B_p\subseteq U]}} 
#*#** We must now show {{M|1=\bigcup_{p\in U}B_p=U}}, we can do this by showing {{M|\bigcup_{p\in U}B_p\subseteq U}} and {{M|\bigcup_{p\in U}B_p\supseteq U}}
#*#**# {{M|\bigcup_{p\in U}B_p\subseteq U}}
#*#**#* Using the [[union of subsets is a subset of the union]] we see:
#*#**#** {{M|\bigcup_{p\in U}B_p\subseteq U]}}
#*#**# {{M|U\subseteq\bigcup_{p\in U}B_p}}
#*#**#* Using the [[implies-subset relation]] we see: {{M|U\subseteq\bigcup_{p\in U}B_p\iff\forall x\in U[x\in\bigcup_{p\in U}B_p]}}, we will show the RHS instead.
#*#**#** Let {{M|x\in U}} be given
#*#**#*** Recall, by definition of [[union]], {{M|x\in\bigcup_{p\in U}B_p\iff\exists q\in U[x\in B_q]}}
#*#**#**** Choose {{M|1=q:=x}} then we have {{M|x\in B_x}} (as {{M|p\in B_p}} is one of the defining conditions of choosing each {{M|B_p}}!)
#*#**#* Thus {{M|U\subseteq\bigcup_{p\in U}B_p}}
#*#** We have shown {{M|1=\bigcup_{p\in U}B_p=U}}
#*#* Since {{M|U\in\mathcal{J}'}} was arbitrary we have shown this for all {{M|U\in\mathcal{J}'}}
#*# We must now show that {{M|\mathcal{B} }} is a '''TBasis''' ''of {{M|(X,\mathcal{J}')}} specifically''. {{Warning|No we do not, but what I did here is useful in proving something else later}}
#*#* Recall that, by definition of {{M|\mathcal{B} }} being a '''GBasis''':
#*#** {{M|1=\forall U\in\mathcal{P}(X)\big[U\in\mathcal{J}'\iff\big(\forall p\in U\exists B\in\mathcal{B}[p\in B\wedge B\subseteq U]\big)\big]}}
#*#* Recall that, by definition of {{M|\mathcal{B} }} being a '''TBasis''' we can talk about open sets as:
#*#** {{M|1=\forall U\in\mathcal{P}(X)\big[U\in\mathcal{J}\iff\big(\forall p\in U\exists B\in\mathcal{B}[p\in B\wedge B\subseteq U]\big)\big]}} (for the topology it is a '''TBasis''' of, {{M|\mathcal{J} }})
#*#* We wish to show that {{M|1=\mathcal{J}'=\mathcal{J} }}
#*#** Let {{M|U\in\mathcal{P}(X)}} be given.
#*#*** Then by definition of {{M|\mathcal{B} }} being a '''GBasis''':
#*#**** {{M|1=U\in\mathcal{J}'\iff\big(\forall p\in U\exists B\in\mathcal{B}[p\in B\wedge B\subseteq U]\big)}}
#*#*** But by definition of {{M|\mathcal{B} }} being a '''TBasis''' (of {{M|\mathcal{J} }}):
#*#**** {{M|1=\big(\forall p\in U\exists B\in\mathcal{B}[p\in B\wedge B\subseteq U]\big)\iff U\in\mathcal{J} }}
#*#*** Combining these we see:
#*#**** {{M|1=U\in\mathcal{J}'\iff\big(\forall p\in U\exists B\in\mathcal{B}[p\in B\wedge B\subseteq U]\big)\iff U\in\mathcal{J} }}
#*#*** Thus: {{M|1=U\in\mathcal{J}'\iff U\in\mathcal{J} }}
#*#** We have shown {{M|1=\forall U\in\mathcal{P}(X)[U\in\mathcal{J}'\iff U\in\mathcal{J}]}}
#*#** For any [[topology]] on {{M|X}}, {{M|\mathcal{K} }} we require: {{M|\mathcal{K}\subseteq\mathcal{P}(X)}}. So,
#*#*** we know: {{M|1=\forall V\in\mathcal{J}[V\in\mathcal{P}(X)]}} (from the [[implies-subset relation]]), and {{M|\forall V'\in\mathcal{J}'[V'\in\mathcal{P}(X)]}}
#*#** We want to show {{M|1=\mathcal{J}=\mathcal{J}'}} remember, we will do this by showing {{M|\mathcal{J}\subseteq\mathcal{J}'}} and {{M|\mathcal{J}'\subseteq\mathcal{J} }}
#*#**# Showing {{M|\mathcal{J}\subseteq\mathcal{J}'}}, using the [[implies-subset relation]] this is the same as showing {{M|\forall V\in\mathcal{J}[V\in\mathcal{J}']}}
#*#**#* Let {{M|V\in\mathcal{J} }} be given.
#*#**#** Then {{M|V\in\mathcal{P}(X)}}
#*#**#** But we know: {{M|\forall W\in\mathcal{P}(X)[W\in\mathcal{J}\iff W\in\mathcal{J}']}}, so we can apply this using {{M|V}}.
#*#**#*** We see {{M|V\in\mathcal{J}\iff V\in\mathcal{J}'}}
#*#**#**** But by definition {{M|V\in\mathcal{J} }} !
#*#**#*** So {{M|V\in\mathcal{J}'}}
#*#**#* Since {{M|V\in\mathcal{J} }} was arbitrary we have shown that for all such {{M|V}} that {{M|V\in\mathcal{J}'}}
#*#**# Showing {{M|\mathcal{J}'\subseteq\mathcal{J} }} is almost exactly the same, so rather than copy and paste and change a few symbols, I'll just say "same as above".
#*#* We have shown that {{M|1=\mathcal{J}=\mathcal{J}'}}
#* This completes the proof.
#* We have shown that if {{M|\mathcal{B} }} is a '''GBasis''' that not only is it a '''TBasis'''
==Notes==
<references group="Note"/>