LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-24

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.

Under the ultrafilter lemma, closure in an ultrafilter-algebra topology is the image of ultrafilters containing the set

Statement

Assume UL/BPI. Let $ξ : β X \to X$ be an ultrafilter algebra, give $X$ its induced topology, and put

$\hat{A} : = {U \in β X : A \in U} .$

Then for every $A \subseteq X$ ,

$\overline{A} = ξ [\hat{A}] .$

Facts & Assumptions

Given: UL/BPI, an ultrafilter algebra $ξ : β X \to X$ , its induced topology, and a subset $A \subseteq X$ .

[L1]

The closure of $A$ is the smallest closed subset containing $A$ (Interior, closure, boundary, exterior, derived set and isolated point in a topological space).

[L2]

The ultrafilter extension principle says that every filter on a set is contained in an ultrafilter on that set (The ultrafilter extension principle (UL/BPI)).

[L3]

Flattening satisfies $B \in μ_{X} (W)$ exactly when $\hat{B} \in W$ (The ultrafilter endofunctor with principal unit and flattening multiplication).

[L4]

An ultrafilter contains exactly one of $C$ and $X ∖ C$ for every $C \subseteq X$ (Characterisation of ultrafilters: every set or its complement).

Proof

technique · direct

1.1

If $x \in A$ , its principal ultrafilter contains $A$ and the algebra unit law gives $ξ (η_{X} (x)) = x$ . Hence $A \subseteq ξ [\hat{A}]$ ; when $A = \emptyset$ , no ultrafilter contains it and both sides of this inclusion are empty.

givenconstruct

1.2

A set $C \subseteq X$ is induced-closed exactly when every ultrafilter containing $C$ has its algebra value in $C$ : this is the complement of the defining induced-open implication, using [L4].

L4algebra

2.1

Put $C = ξ [\hat{A}]$ and fix an ultrafilter $V$ with $C \in V$ . On $β X$ , the family consisting of $\hat{A}$ and all $ξ^{- 1} [B]$ for $B \in V$ has the finite-intersection property: for a finite intersection $B$ of members of $V$ , choose $x \in B \cap C$ and then an ultrafilter in $\hat{A}$ mapping to $x$ . By [L2], extend this family to an ultrafilter $W$ on $β X$ .

step 1.2L2choose

3.1

Since $\hat{A} \in W$ , [L3] gives $A \in μ_{X} (W)$ . Since every $ξ^{- 1} [B]$ with $B \in V$ lies in $W$ , maximality gives $β (ξ) (W) = V$ . The algebra multiplication law yields $ξ (V) = ξ μ_{X} (W) \in ξ [\hat{A}] = C$ . Thus $C$ is induced-closed by step 1.2.

step 2.1L3algebra

4.1

If $D$ is any induced-closed superset of $A$ , every ultrafilter containing $A$ contains $D$ , so step 1.2 gives $ξ [\hat{A}] \subseteq D$ . By steps 1.1 and 3.1, $ξ [\hat{A}]$ is itself a closed superset of $A$ , hence it is the closure by [L1]. This also gives $\overline{\emptyset} = \emptyset$ .

step 1.1step 3.1L1∎

Depends on

Used by

Under the ultrafilter lemma, an ultrafilter algebra maps each ultrafilter to its unique limit Lemma

Dependency tree · two levels

16 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

J. Goubault-Larrecq, Algebras of filter-related monads: I. Ultrafilters and Manes' theorem, Lemma A (standard reference, not scraped)