ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passaudited 2026-07-31

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.

An ultrafilter selects exactly one cell of a finite disjoint list whose union it contains

Example

Let $U$ be an ultrafilter on $X$ , let $n \in N$ , and let $s : n \to P (X)$ be a finite list of pairwise disjoint sets. If

$⋃_{i \in n} s (i) \in U,$

then there is a unique $i \in n$ such that $s (i) \in U$ . The selected cell is necessarily nonempty. In particular, for a finite partition of $X$ into nonempty cells, $U$ selects exactly one cell.

The empty list causes no exceptional conclusion: its union is $\emptyset$ , so the displayed hypothesis is false for a proper filter.

Facts & Assumptions

Given: An ultrafilter $U$ on $X$ , a natural number $n$ , and a list $s : n \to P (X)$ such that $s (i) \cap s (j) = \emptyset$ whenever $i \neq j$ , and whose union belongs to $U$ .

[L1]

For every $n \in N$ and every list $s : n \to P (X)$ , if $⋃_{i \in n} s (i) \in U$ , then $s (i) \in U$ for some $i \in n$ (Ultrafilters are prime: a union in $U$ has a member in $U$ ).

[F1]

A filter omits $\emptyset$ and is closed under pairwise intersection (Filter on a set).

[F2]

In the von Neumann natural numbers, $n$ is the set of its predecessors, so a map $s : n \to P (X)$ is a finite list indexed by $i \in n$ (The natural numbers $N$ (von Neumann)).

Verification

technique · direct

1.1givenL1

By [L1], there is an index $i \in n$ with $s (i) \in U$ .

1.2givenF1

If distinct indices $i, j \in n$ both satisfied $s (i), s (j) \in U$ , then pairwise disjointness and intersection closure would give $\emptyset = s (i) \cap s (j) \in U$ , contradicting properness.

2.1step 1.1F1

This selected cell is nonempty, because $s (i) = \emptyset$ would put $\emptyset$ in the proper filter $U$ .

3.1step 1.1step 2.1step 1.2

Step 1.1 gives existence and step 1.2 gives uniqueness, while step 2.1 shows the selected cell is nonempty.

4.1step 3.1F1F2∎

When the listed sets are nonempty and partition $X$ , their union is $X \in U$ , so step 3.1 says that exactly one partition cell belongs to $U$ .

Depends on

Used by

Nothing in the library uses this result yet.

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)