TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Characterisation of ultrafilters: every set or its complement

Statement

Let $X$ be a set and $U$ a filter on $X$ (Filter on a set). The following are equivalent:

$U$ is an ultrafilter on $X$ (Ultrafilter);
for every $A \subseteq X$ , either $A \in U$ or $X ∖ A \in U$ .

Moreover, for any filter the two alternatives are exclusive: never both $A \in U$ and $X ∖ A \in U$ . So an ultrafilter decides every subset of $X$ , containing exactly one of $A$ and $X ∖ A$ .

Facts & Assumptions

Given: A set $X$ and a filter $U$ on $X$ .

[A1]

$U$ is a filter on $X$ : $X \in U$ , $\emptyset \notin U$ , $U$ is closed under pairwise intersection, and $B \in U$ whenever $A \in U$ and $A \subseteq B \subseteq X$ (Filter on a set).

[L1]

An ultrafilter on $X$ is a filter that is maximal for inclusion among the filters on $X$ ; maximality of $m$ says that $m \leq x$ forces $x = m$ (Ultrafilter, Maximal element and greatest element).

Proof

technique · direct

1.1

Exclusivity, for any filter. If $A$ and $X ∖ A$ both lay in $U$ then so would $A \cap (X ∖ A) = \emptyset$ , which properness forbids.

1.2

Forward. Assume statement 1, let $A \subseteq X$ , and suppose $X ∖ A \notin U$ ; the goal is $A \in U$ .

assume-hyp

1.3

Forward. Let $G = {B \subseteq X : C \cap A \subseteq B for some C \in U}$ .

construct

2.1

Forward. Every $C \in U$ satisfies $C \cap A \neq \emptyset$ : from $C \cap A = \emptyset$ one gets $C \subseteq X ∖ A$ , and upward closure would then put $X ∖ A$ into $U$ , which step 1.2 excludes.

step 1.2A1

2.2

Forward. $U \subseteq G$ , since $C \cap A \subseteq C$ for $C \in U$ ; and $A \in G$ , since $X \in U$ and $X \cap A \subseteq A \subseteq X$ .

step 1.3A1

2.3

Converse. Assume statement 2 and let $H$ be any filter on $X$ with $U \subseteq H$ ; for $A \in H$ one cannot have $X ∖ A \in U$ , since then $X ∖ A \in H$ and $\emptyset = A \cap (X ∖ A) \in H$ , against properness of $H$ .

step 1.1A1assume-hyp

3.1

Forward. $G$ is a filter on $X$ : its members are subsets of $X$ by definition; $X \in G$ by step 2.2; $\emptyset \notin G$ , because $C \cap A \subseteq \emptyset$ would make $C \cap A$ empty against step 2.1; it is closed upward in $X$ by transitivity of $\subseteq$ ; and if $C_{1} \cap A \subseteq B_{1}$ and $C_{2} \cap A \subseteq B_{2}$ with $C_{1}, C_{2} \in U$ then $(C_{1} \cap C_{2}) \cap A \subseteq B_{1} \cap B_{2}$ with $C_{1} \cap C_{2} \in U$ , so $B_{1} \cap B_{2} \in G$ .

step 1.3step 2.1step 2.2A1

3.2

Converse. So $A \in U$ for every $A \in H$ by statement 2, giving $H \subseteq U$ and hence $H = U$ ; no filter strictly contains $U$ , so $U$ is maximal and statement 2 implies statement 1.

step 2.3L1

4.1

Forward. Maximality of $U$ applied to the filter $G \supseteq U$ gives $G = U$ , hence $A \in U$ by step 2.2; so statement 1 implies statement 2.

step 3.1step 2.2step 1.2L1

5.1

The two statements are therefore equivalent, and by step 1.1 an ultrafilter contains exactly one of $A$ and $X ∖ A$ for each $A \subseteq X$ .

step 4.1step 3.2step 1.1∎

Remarks

This is the working form of the definition. Maximality is a statement about the whole poset of filters; deciding complements is a statement about $U$ alone, and it is what one actually checks and uses. It is the route taken by Ultrafilters are prime: a union in $U$ has a member in $U$ , for instance. It is not the only route: FALSE, once the ultrafilter lemma is available: every ultrafilter is principal is refuted from properness and the ultrafilter lemma directly, without this characterisation, and does not list it among its dependencies.
The two directions run as separate threads, and the mechanical stratification interleaves them, so each step is labelled Forward or Converse. They share nothing except the filter $U$ and the exclusivity of step 1.1: the forward thread builds a specific filter $G$ , the converse thread argues about an arbitrary filter $H$ above $U$ .
The filter $G$ built at step 1.3 is the filter generated by $U \cup {A}$ (A family lies in a filter exactly when it has the finite intersection property): its members are the supersets of the sets $C \cap A$ with $C \in U$ . Those sets are not all the intersections of finite lists drawn from $U \cup {A}$ , since a list omitting $A$ intersects to a member $C$ of $U$ and not to a set of the form $C \cap A$ . The two families generate the same filter all the same: finitely many members of $U$ intersect to a single $C \in U$ , so every such finite intersection either is a $C$ or is a $C \cap A$ , and in the first case it contains $C \cap A$ ; conversely each $C \cap A$ is itself one of the finite intersections. The upward closures therefore coincide, which is all that "generated by" asks. Step 2.1 is the check that $U \cup {A}$ has the finite intersection property, and that check is exactly where $X ∖ A \notin U$ is used.
Exclusivity is a property of filters, not of ultrafilters, and it holds for the trivial reason that $A$ and $X ∖ A$ are disjoint. What maximality buys is only the "at least one" half. Reading the characterisation as a two-valued decision on $P (X)$ makes an ultrafilter a finitely additive ${0, 1}$ -valued measure on $X$ , which is the standard way it is used.
The characterisation makes ultrafilters visibly rigid: $U$ is determined by which of each complementary pair it takes, so an ultrafilter is a consistent choice on all of $P (X)$ at once. This is why producing one in general is done here from a choice principle rather than by a construction (The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter).

Depends on

Used by

Dependency tree · two levels

14 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Ultrafilter (set theory) (Wikipedia) (standard reference, not scraped)
Ultrafilter (Wikipedia) (standard reference, not scraped)