IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory Ultrafilter_ZF imports Topology_ZF_4 Topology_ZF_examples

begin

This theory deals with ultrafilters; which is a maximal filter.

Ultrafilters

In this section we define ultrafilters and prove their basic properties.

An ultrafilter is a filter that is maximal, i.e. not properly contained in any other filter.

definition

\( \mathfrak{F} \text{ is an ultrafilter on }X \equiv (\mathfrak{F} \text{ is a filter on }X) \wedge (\forall \mathfrak{G} .\ (\mathfrak{G} \text{ is a filter on }X) \longrightarrow (\mathfrak{F} \subseteq \mathfrak{G} \longrightarrow \mathfrak{G} = \mathfrak{F} )) \)

Every set or its opposite is in an ultrafilter

lemma set_ultrafilter:

assumes \( A\in Pow(X) \), \( \mathfrak{F} \text{ is an ultrafilter on }X \)

shows \( A\in \mathfrak{F} \vee (X-A)\in \mathfrak{F} \)proof

from assms(2) have filter: \( \mathfrak{F} \text{ is a filter on }X \) unfolding IsUltrafilter_def

{

assume a0: \( A\neq 0 \)

{

assume a: \( A\notin \mathfrak{F} \), \( X-A\notin \mathfrak{F} \)

have \( A \in Pow(X) \Longrightarrow \mathfrak{F} \text{ is a filter on } X \Longrightarrow A \neq \emptyset \Longrightarrow \) \( A \notin \mathfrak{F} \Longrightarrow (X \setminus A) \notin \mathfrak{F} \Longrightarrow \exists \mathfrak{G} .\ ((\mathfrak{G} \text{ is a filter on } X) \wedge A \in \mathfrak{G} \wedge \mathfrak{F} \subseteq \mathfrak{G} ) \) using extend_filter

with a, assms(1), a0, filter obtain \( \mathfrak{G} \) where g: \( \mathfrak{G} \text{ is a filter on }X \), \( A \in \mathfrak{G} \), \( \mathfrak{F} \subseteq \mathfrak{G} \)

with assms(2) have \( A\in \mathfrak{F} \) unfolding IsUltrafilter_def

with a have \( False \)

}

then have \( A\in \mathfrak{F} \vee (X-A)\in \mathfrak{F} \)

}

moreover {

assume \( A=0 \)

then have \( X-A=X \)

then have \( X-A\in \mathfrak{F} \) using filter unfolding IsFilter_def

then have \( A\in \mathfrak{F} \vee (X-A)\in \mathfrak{F} \)

} ultimately show \( A\in \mathfrak{F} \vee (X-A)\in \mathfrak{F} \)

qed

It contains only one of them

lemma only_set_or_opposite:

assumes \( A\in Pow(X) \), \( \mathfrak{F} \text{ is a filter on }X \), \( A\in \mathfrak{F} \)

shows \( (X-A)\notin \mathfrak{F} \)proof

assume \( X-A\in \mathfrak{F} \)

with assms have \( A\cap (X-A)\in \mathfrak{F} \) using is_filter_def_split(4)

moreover

have \( A\cap (X-A) = 0 \)

ultimately have \( 0\in \mathfrak{F} \)

then show \( False \) using assms(2), is_filter_def_split(1)

qed

If a filter contains a set or its opposite, it is in an ultrafilter

lemma set_ultrafilter_equiv:

assumes \( \mathfrak{F} \text{ is a filter on }X \), \( \forall A\in Pow(X).\ A\in \mathfrak{F} \vee (X-A)\in \mathfrak{F} \)

shows \( \mathfrak{F} \text{ is an ultrafilter on }X \)proof

from assms(1) have I: \( \mathfrak{F} \text{ is a filter on }X \)

{

fix \( \mathfrak{G} \)

assume g: \( \mathfrak{G} \text{ is a filter on }X \), \( \mathfrak{F} \subseteq \mathfrak{G} \)

{

assume \( \mathfrak{G} \neq \mathfrak{F} \)

with g(2) obtain \( h \) where h: \( h:\mathfrak{G} \), \( h\notin \mathfrak{F} \)

from h(1), g(1) have \( h\in Pow(X) \), \( h\neq 0 \) unfolding IsFilter_def

with assms(2), h(2) have \( X-h\in \mathfrak{F} \)

with g(2) have \( X-h:\mathfrak{G} \)

with h(1), g(1) have \( (X-h)\cap h\in \mathfrak{G} \) unfolding IsFilter_def

moreover

have \( (X-h)\cap h=0 \)

ultimately have \( 0\in \mathfrak{G} \)

with g(1) have \( False \) unfolding IsFilter_def

}

then have \( \mathfrak{G} =\mathfrak{F} \)

}

then have II: \( \forall \mathfrak{G} .\ (\mathfrak{G} \text{ is a filter on } X) \longrightarrow \mathfrak{F} \subseteq \mathfrak{G} \longrightarrow \mathfrak{G} =\mathfrak{F} \)

from I, II show \( thesis \) unfolding IsUltrafilter_def

qed

Filters of containing a point, are ultrafilters

lemma include_point_ultrafilter:

assumes \( x\in X \)

shows \( \{A\in Pow(X).\ x\in A}\text{ is an ultrafilter on }\} \)proof

have I: \( 0\notin \{A \in Pow(X) .\ x \in A\} \)

from assms have II: \( X\in \{A \in Pow(X) .\ x \in A\} \)

have III: \( \{A \in Pow(X) .\ x \in A\} \subseteq Pow(X) \)

{

fix \( A \) \( B \)

assume AB: \( A\in \{A \in Pow(X) .\ x \in A\} \), \( B\in \{A \in Pow(X) .\ x \in A\} \)

then have \( A\cap B\in \{A \in Pow(X) .\ x \in A\} \)

}

then have IV: \( \forall A\in \{A \in Pow(X) .\ x \in A\}.\ \forall B\in \{A \in Pow(X) .\ x \in A\}.\ A\cap B\in \{A \in Pow(X) .\ x \in A\} \)

{

fix \( B \) \( C \)

assume B: \( B\in \{A \in Pow(X) .\ x \in A\} \), \( C\in Pow(X) \), \( B\subseteq C \)

then have \( C\in \{A \in Pow(X) .\ x \in A\} \)

}

then have V: \( \forall B\in \{A \in Pow(X) .\ x \in A\}.\ \forall C\in Pow(X).\ B \subseteq C \longrightarrow C\in \{A \in Pow(X) .\ x \in A\} \)

from I, II, III, IV, V have I: \( \{A \in Pow(X) .\ x \in A\} \text{ is a filter on } X \) unfolding IsFilter_def

{

fix \( A \)

assume A: \( A\in Pow(X) \)

have \( x:A \vee x\notin A \)

with assms have \( x\in A \vee x\in X-A \)

with A(1) have \( A\in \{A \in Pow(X) .\ x \in A\} \vee X-A: \{A \in Pow(X) .\ x \in A\} \)

}

then have II: \( \forall A\in Pow(X).\ A \in \{A \in Pow(X) .\ x \in A\} \vee X - A \in \{A \in Pow(X) .\ x \in A\} \)

from I, II show \( thesis \) using set_ultrafilter_equiv

qed

An ultrafilter that has no singleton sets, does not have finite sets

lemma ultrafilter_finite_set:

assumes \( \mathfrak{F} \text{ is an ultrafilter on }X \), \( \forall x\in X.\ \{x\}\notin \mathfrak{F} \), \( A\in \text{FinPow}(X) \)

shows \( A\notin \mathfrak{F} \)proof

from assms(1) have I: \( 0\notin \mathfrak{F} \) unfolding IsUltrafilter_def, IsFilter_def

have III: \( A\in \text{FinPow}(X) \) using assms(3)

{

fix \( B \)

assume b: \( B\in \text{FinPow}(X) \), \( B\notin \mathfrak{F} \)

{

fix \( s \)

assume s: \( s\in X \)

{

assume cont: \( B\cup \{s\}\in \mathfrak{F} \)

{

assume \( B=0 \)

then have \( B\cup \{s\} = \{s\} \)

with s, assms(2), cont have \( False \)

}

moreover {

assume \( B\neq 0 \)

with b have \( X-B \in \mathfrak{F} \) using assms(1), set_ultrafilter unfolding FinPow_def

moreover

have \( \{s\} \in Pow(X) \Longrightarrow \mathfrak{F} \text{ is an ultrafilter on }X \Longrightarrow \) \( \{s\} \in \mathfrak{F} \vee X \setminus \{s\} \in \mathfrak{F} \) using set_ultrafilter

with assms(1,2), s have \( X-\{s\}\in \mathfrak{F} \)

ultimately have \( (X-B)\cap (X-\{s\}) \in \mathfrak{F} \) using assms(1) unfolding IsUltrafilter_def, IsFilter_def

moreover {

fix \( q \)

assume \( q\in (X-B)\cap (X-\{s\}) \)

then have \( q:X \), \( q\notin B \), \( q\notin \{s\} \)

then have \( q\in X-(B\cup \{s\}) \)

}

then have \( (X-B)\cap (X-\{s\}) \subseteq X-(B\cup \{s\}) \)

moreover

have \( X-(B\cup \{s\})\in Pow(X) \)

ultimately have \( X-(B\cup \{s\}) \in \mathfrak{F} \) using assms(1) unfolding IsFilter_def, IsUltrafilter_def

with cont have \( (X-(B\cup \{s\}))\cap (B\cup \{s\}): \mathfrak{F} \) using assms(1) unfolding IsFilter_def, IsUltrafilter_def

moreover {

fix \( q \)

assume \( q\in (X-(B\cup \{s\}))\cap (B\cup \{s\}) \)

then have \( False \)

}

then have \( (X-(B\cup \{s\}))\cap (B\cup \{s\}) = 0 \)

ultimately have \( 0: \mathfrak{F} \)

with assms(1) have \( False \) unfolding IsUltrafilter_def, IsFilter_def

} ultimately have \( False \)

}

then have \( B\cup \{s\}\notin \mathfrak{F} \)

}

then have \( \forall q\in X.\ B \cup \{q\} \notin \mathfrak{F} \)

}

then have II: \( \forall A\in \text{FinPow}(X).\ A \notin \mathfrak{F} \longrightarrow (\forall q\in X.\ A \cup \{q\} \notin \mathfrak{F} ) \)

from I, II, III show \( thesis \) by (rule FinPow_induct )

qed

The cofinite filter plays an important role in ultrafilters.

corollary ultrafilter_contains_cofinite:

assumes \( \mathfrak{F} \text{ is an ultrafilter on }X \), \( \forall x\in X.\ \{x\}\notin \mathfrak{F} \)

shows \( (CoFinite(X))-\{0\} \subseteq \mathfrak{F} \)proof

fix \( S \)

assume \( S\in (CoFinite(X))-\{0\} \)

then have s: \( S \in Pow(X) \), \( X - S \prec nat \), \( S\neq 0 \) unfolding CoCardinal_def, Cofinite_def

then have \( Finite(X-S) \) using lesspoll_nat_is_Finite

then have \( X-S\in \text{FinPow}(X) \) unfolding FinPow_def

with ultrafilter_finite_set, assms have \( X-S\notin \mathfrak{F} \)

with assms(1) show \( S\in \mathfrak{F} \) using set_ultrafilter, s(1,3)

qed

An ultrafilter is free or principal.

corollary ultrafilter_principal_or_free:

assumes \( \mathfrak{F} \text{ is an ultrafilter on }X \)

shows \( \bigcap \mathfrak{F} = 0 \vee (\exists x\in X.\ \bigcap \mathfrak{F} = \{x\}) \)proof

{

assume \( \neg (\exists x\in X.\ \bigcap \mathfrak{F} = \{x\}) \)

then have r: \( \forall x\in X.\ \bigcap \mathfrak{F} \neq \{x\} \)

from assms have a: \( X\neq 0 \) unfolding IsUltrafilter_def, IsFilter_def

{

fix \( x \)

assume x: \( x:X \), \( \{x\}:\mathfrak{F} \)

from this(2), assms have \( \forall C\in Pow(X).\ \{x\} \subseteq C \longrightarrow C \in \mathfrak{F} \) unfolding IsFilter_def, IsUltrafilter_def

then have s: \( \{C\in Pow(X).\ x\in C\} \subseteq \mathfrak{F} \)

{

fix \( q \)

assume q: \( q\in \mathfrak{F} \), \( x\notin q \)

from q(2), s, x(1) have \( X-q:\mathfrak{F} \)

with q(1) have \( (X-q)\cap q\in \mathfrak{F} \) using assms unfolding IsUltrafilter_def, IsFilter_def

moreover

have \( (X-q)\cap q = 0 \)

ultimately have \( 0:\mathfrak{F} \)

with assms have \( False \) unfolding IsUltrafilter_def, IsFilter_def

}

then have \( \mathfrak{F} \subseteq \{C\in Pow(X).\ x\in C\} \) using assms unfolding IsUltrafilter_def, IsFilter_def

with s have \( \mathfrak{F} =\{C\in Pow(X).\ x\in C\} \)

then have \( \bigcap \mathfrak{F} =\{x\} \) using x(2)

with r, x(1) have \( False \)

}

then have \( \forall x\in X.\ \{x\}\notin \mathfrak{F} \)

then have sub: \( ( \text{Cofinite}(X))-\{0\} \subseteq \mathfrak{F} \) using ultrafilter_contains_cofinite, assms

have \( ( \text{Cofinite}(X))\text{ is a topology } \) using CoCar_is_topology, InfCard_nat unfolding Cofinite_def

then have \( \bigcup \text{Cofinite}(X)\in \text{Cofinite}(X) \) using carr_open

then have b: \( X \in ( \text{Cofinite}(X)) \) using union_cocardinal unfolding Cofinite_def

from a, b have \( X\in ( \text{Cofinite}(X))-\{0\} \)

with sub have A: \( \bigcap \mathfrak{F} \subseteq \bigcap (( \text{Cofinite}(X))-\{0\}) \)

{

fix \( q \)

assume q: \( q\in \bigcap (( \text{Cofinite}(X))-\{0\}) \)

from a, b have B: \( \bigcap (( \text{Cofinite}(X))-\{0\}) \subseteq X \)

with q have qX: \( q\in X \)

then have \( X-(X-\{q\}) = \{q\} \)

then have \( X-(X-\{q\})\approx 1 \) using singleton_eqpoll_1

then have \( X-(X-\{q\}) \prec nat \) using eq_lesspoll_trans, n_lesspoll_nat, nat_1I

then have cof: \( X-\{q\}\in ( \text{Cofinite}(X)) \) unfolding Cofinite_def, CoCardinal_def

{

assume \( X-\{q\} = 0 \)

with qX have \( X=\{q\} \)

then have \( \bigcap \mathfrak{F} \subseteq \{q\} \) using assms unfolding IsUltrafilter_def, IsFilter_def

with qX, r have \( \bigcap \mathfrak{F} = 0 \)

}

moreover {

assume \( X-\{q\} \neq 0 \)

with cof have \( X-\{q\}\in ( \text{Cofinite}(X)) -\{0\} \)

then have \( \bigcap (( \text{Cofinite}(X))-\{0\}) \subseteq X-\{q\} \)

with q have \( False \)

then have \( \bigcap \mathfrak{F} = 0 \)

} ultimately have \( \bigcap \mathfrak{F} = 0 \)

}

then have \( \bigcap \mathfrak{F} =0 \vee \bigcap (( \text{Cofinite}(X))-\{0\}) = 0 \)

with A have \( \bigcap \mathfrak{F} =0 \)

}

then show \( thesis \)

qed

end

Definition of IsUltrafilter: \( \mathfrak{F} \text{ is an ultrafilter on }X \equiv (\mathfrak{F} \text{ is a filter on }X) \wedge (\forall \mathfrak{G} .\ (\mathfrak{G} \text{ is a filter on }X) \longrightarrow (\mathfrak{F} \subseteq \mathfrak{G} \longrightarrow \mathfrak{G} = \mathfrak{F} )) \)

lemma extend_filter:

assumes \( A\in Pow(X) \), \( \mathfrak{F} \text{ is a filter on } X \), \( A\neq 0 \), \( A\notin \mathfrak{F} \), \( X\setminus A\notin \mathfrak{F} \)

shows \( \exists \mathfrak{G} .\ (\mathfrak{G} \text{ is a filter on } X) \wedge A\in \mathfrak{G} \wedge \mathfrak{F} \subseteq \mathfrak{G} \)

Definition of IsFilter: \( \mathfrak{F} \text{ is a filter on } X \equiv (\emptyset \notin \mathfrak{F} ) \wedge (X\in \mathfrak{F} ) \wedge \mathfrak{F} \subseteq Pow(X) \wedge \) \( (\forall A\in \mathfrak{F} .\ \forall B\in \mathfrak{F} .\ A\cap B\in \mathfrak{F} ) \wedge (\forall B\in \mathfrak{F} .\ \forall C\in Pow(X).\ B\subseteq C \longrightarrow C\in \mathfrak{F} ) \)

lemma is_filter_def_split:

assumes \( \mathfrak{F} \text{ is a filter on } X \)

shows \( \emptyset \notin \mathfrak{F} \), \( X\in \mathfrak{F} \), \( \mathfrak{F} \subseteq Pow(X) \), \( \forall A\in \mathfrak{F} .\ \forall B\in \mathfrak{F} .\ A\cap B\in \mathfrak{F} \) and \( \forall B\in \mathfrak{F} .\ \forall C\in Pow(X).\ B\subseteq C \longrightarrow C\in \mathfrak{F} \)

lemma is_filter_def_split:

assumes \( \mathfrak{F} \text{ is a filter on } X \)

lemma set_ultrafilter_equiv:

assumes \( \mathfrak{F} \text{ is a filter on }X \), \( \forall A\in Pow(X).\ A\in \mathfrak{F} \vee (X-A)\in \mathfrak{F} \)

shows \( \mathfrak{F} \text{ is an ultrafilter on }X \)

lemma set_ultrafilter:

assumes \( A\in Pow(X) \), \( \mathfrak{F} \text{ is an ultrafilter on }X \)

shows \( A\in \mathfrak{F} \vee (X-A)\in \mathfrak{F} \)

Definition of FinPow: \( \text{FinPow}(X) \equiv \{A \in Pow(X).\ Finite(A)\} \)

theorem FinPow_induct:

assumes \( P(0) \) and \( \forall A \in \text{FinPow}(X).\ P(A) \longrightarrow (\forall a\in X.\ P(A \cup \{a\})) \) and \( B \in \text{FinPow}(X) \)

shows \( P(B) \)

Definition of CoCardinal: \( \text{CoCardinal}(X,T) \equiv \{F\in Pow(X).\ X-F \prec T\}\cup \{0\} \)

Definition of Cofinite: \( CoFinite X \equiv \text{CoCardinal}(X,nat) \)

corollary ultrafilter_contains_cofinite:

assumes \( \mathfrak{F} \text{ is an ultrafilter on }X \), \( \forall x\in X.\ \{x\}\notin \mathfrak{F} \)

shows \( (CoFinite(X))-\{0\} \subseteq \mathfrak{F} \)

lemma CoCar_is_topology:

assumes \( InfCard (Q) \)

shows \( \text{CoCardinal}(X,Q) \text{ is a topology } \)

lemma carr_open:

assumes \( T \text{ is a topology } \)

shows \( (\bigcup T) \in T \)