Filter Basis Generates Filter

From ProofWiki
Jump to: navigation, search

Theorem

Let $X$ be a set, and $\mathcal P \left({X}\right)$ be the power set of $X$.

Let $\mathcal B \subset \mathcal P \left({X}\right)$.


Then:

$\mathcal F = \left\{{V \subseteq X: \exists U \in \mathcal B: U \subseteq V}\right\}$ is a filter on $X$

iff:

$(1): \quad \forall V_1, V_2 \in \mathcal B: \exists U \in \mathcal B: U \subseteq V_1 \cap V_2$
$(2): \quad \varnothing \not \in \mathcal B, \mathcal B \ne \varnothing$


That is, $\mathcal B$ is a filter basis of the filter $\mathcal F$, which is generated by $\mathcal B$.


Proof

Assume first that $\mathcal F$ is a filter on $X$.

Then $X \in \mathcal F$ and thus $\mathcal B \ne \varnothing$.

Because $\varnothing \not \in \mathcal F$ we have that $\varnothing \not \in \mathcal B$, since $\mathcal B \subseteq \mathcal F$.


Let $V_1, V_2 \in \mathcal B$, then $V_1, V_2 \in \mathcal F$.

Because $\mathcal F$ is a filter it follows that $V := V_1 \cap V_2 \in \mathcal F$.

The definition of $\mathcal F$ implies therefore that there is $U \in \mathcal B$ such that $U \subseteq V = V_1 \cap V_2$.


Assume now that $\mathcal B$ satisfies conditions $(1)$ and $(2)$.

To show that $\mathcal F$ is a filter, note that because $\mathcal B \ne \varnothing$ there is a $B \in \mathcal B$.

Because $\mathcal B \subset \mathcal P \left({X}\right)$ we know that $B \subseteq X$ and thus $X \in \mathcal F$ by the definition of $\mathcal F$.

Since the only subset of $\varnothing$ is $\varnothing$ and since $\varnothing \not \in \mathcal B$ it follows that $\varnothing \not \in \mathcal F$.

Let $V_1, V_2 \in \mathcal F$.

Then there exist $U_1, U_2 \in \mathcal B$ such that $U_1 \subseteq V_1$ and $U_2 \subseteq V_2$.

Because $\mathcal B$ satisfies condition (1) there exists a set $U \in \mathcal B$ for which $U \subseteq U_1 \cap U_2$ holds.

Since $U_1 \cap U_2 \subseteq V_1 \cap V_2$ this implies that $U \subseteq V_1 \cap V_2$ and therefore $V_1 \cap V_2 \in \mathcal F$.

$\blacksquare$


Sources

Personal tools
Namespaces
Variants
Actions
Navigation
ProofWiki.org
ToDo
Toolbox
Google AdSense