LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 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.

The open-set family induced by an ultrafilter algebra is a topology

Statement

For every ultrafilter algebra $ξ : β X \to X$ , the family $τ_{ξ}$ of induced-open subsets is a topology on $X$ .

Facts & Assumptions

Given: An ultrafilter algebra $ξ : β X \to X$ and its induced-open family $τ_{ξ}$ .

[L1]

A subset $O \subseteq X$ is induced-open when $ξ (U) \in O$ implies $O \in U$ for every ultrafilter $U$ on $X$ (The open-set family induced by an ultrafilter algebra).

[L2]

A topology contains the empty set and whole space, is closed under arbitrary unions, and is closed under finite intersections (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

Proof

technique · direct

1.1

The empty set is induced-open because its antecedent never holds, and $X$ is induced-open because every ultrafilter contains $X$ .

L1algebra

1.2

Let $(O_{i})_{i \in I}$ be induced-open and suppose $ξ (U) \in ⋃_{i} O_{i}$ . Some $O_{i}$ contains $ξ (U)$ , hence $O_{i} \in U$ by [L1], and upward closure gives $⋃_{i} O_{i} \in U$ . Thus arbitrary unions are induced-open.

L1algebra

2.1

If $O$ and $V$ are induced-open and $ξ (U) \in O \cap V$ , then $O, V \in U$ by [L1], so $O \cap V \in U$ . This also covers the empty and singleton finite intersections using step 1.1.

L1algebra

3.1

Steps 1.1, 1.2, and 2.1 verify the axioms in [L2], so $τ_{ξ}$ is a topology. No extension of a filter and no choice principle was used.

step 1.1step 1.2step 2.1L2∎

Depends on

Used by

Cited to discharge well-definedness by The open-set family induced by an ultrafilter algebra.

Dependency tree · two levels

9 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 (standard reference, not scraped)