Basis for a topology

Definition

Let $X$ be a set. A basis for a topology on $X$ is a collection of subsets of $X$ , $\mathcal{B}\subseteq\mathcal{P}(X)$ such that^[1]:

$\forall x\in X\exists B\in\mathcal{B}[x\in B]$ - every element of $X$ belongs to at least one basis element.
$\forall B_1,B_2\in\mathcal{B},x\in X\ \exists B_3\in\mathcal{B}[x\in B_1\cap B_2\implies(x\in B_3\wedge B_3\subseteq B_1\cap B_2)]$ ^{[Note 1]} - if any 2 basis elements have non empty intersection, there is a basis element within that intersection containing each point in it.

Note that:

If $\mathcal{B}$ is such a basis for $X$ , we define the topology $\mathcal{J}$ generated by $\mathcal{B}$ ^[1] as follows:

A subset of X, U⊆X is considered open (equivalently, U∈J) if:
- $\forall x\in U\exists B\in\mathcal{B}[x\in B\wedge B\subseteq U]$ ^{[Note 2]}

[Expand]
Claim: This $\mathcal{(J)}$ is indeed a topology

Jump up ↑
This is a great example of a hiding if-and-only-if, note that:
- (x∈B3∧B3⊆B1∩B2)⟹x∈B1∩B2 (by the implies-subset relation) so we have:
  - $(x\in B_3\wedge B_3\subseteq B_1\cap B_2)\implies x\in B_1\cap B_2\implies(x\in B_3\wedge B_3\subseteq B_1\cap B_2)$
- Thus $(x\in B_3\wedge B_3\subseteq B_1\cap B_2)\iff x\in B_1\cap B_2$
This pattern occurs a lot, like with the axiom of extensionality in set theory.
Jump up ↑ Note that each basis element is itself is open. This is because $U$ is considered open if forall x, there is a basis element containing $x$ with that basis element $\subseteq U$ , if $U$ is itself a basis element, it clearly satisfies this as $B\subseteq B$

TODO: Make this into a claim