Alphabeta Math
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.

✓ 18 results · all verified · 17 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Convergence: Nets and Filters

1 · Prerequisites

2 · Summary

Open-cover compactness is equivalent to the closed finite-intersection condition, while filters and ultrafilters record upward-closed families of subsets. Neighbourhoods, closure and continuity provide the local topology used here; countable choice enters the published first-countability sequence criterion, and the ultrafilter lemma is stated whenever an ultrafilter extension is used.

Directed preorders, nets, eventuality, subnets and net convergence first characterize closure, continuity and Hausdorff separation. Tail filters and derived nets then give the net-filter dictionary. Universal nets and ultrafilters yield the compactness equivalences and the compact Hausdorff product theorem under the ultrafilter lemma. Fréchet–Urysohn and sequential spaces finish the development with the first-countability implication hierarchy.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

Directed preorders and nets

Definition

A directed preorder is a nonempty set D with a reflexive, transitive relation ≤ such that every d,e∈D have a common upper bound: some f∈D satisfies d≤f and e≤f. Antisymmetry is not required; thus this is a preorder obtained by omitting antisymmetry from the partial-order axioms of Partial order and partially ordered set.

If X is the underlying set of a topological space (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison), a net in X indexed by D is a function x:D→X, written (xd)d∈D. The order on D records which indices are sufficiently far along; it need not be a linear order.

Remarks

Some texts require a directed set to be a partial order. The present preorder convention is deliberate: none of the convergence arguments needs antisymmetry, and it permits convenient index systems with equivalent stages.

DefinitionDefinition: Literature-sourcedProof: AI-generatedjudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

A net is eventually or frequently in a subset of its codomain

Definition

Let x:D→X be a net (Directed preorders and nets) and let S⊆X.

  • x is eventually in S if some d0∈D satisfies xd∈S for every d≥d0.
  • x is frequently in S if, for every d0∈D, there is d≥d0 with xd∈S.

The net is frequently in S exactly when it is not eventually in X∖S: negating the first displayed existential-universal condition gives the second one.

DefinitionDefinition: Literature-sourcedProof: AI-generatedjudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

Convergence and cluster points of a net in a topological space

Definition

Let x:D→X be a net in a topological space X and let p∈X.

Convergence implies being a cluster point. If x is eventually in a neighbourhood N after d0, then for an arbitrary threshold d choose a common upper bound e≥d,d0; one has xe∈N, so x is frequently in N.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

Subnet via an eventually cofinal index map

Definition

Let x:D→X be a net. A net y:E→X is a subnet of x if E is a directed preorder and there is a map ϕ:E→D such that ye=xϕ(e) for every e∈E and

for every d∈D there is e0∈E such that e≥e0⟹ϕ(e)≥d.

The displayed condition says that ϕ is eventually cofinal. No order-preservation condition is imposed on ϕ.

Remarks

Stricter conventions require ϕ to be order-preserving, or formulate subnets through a relation. They are not used here. Eventual cofinality is the property needed to carry eventual statements from a net to its subnet and to turn cluster points into convergent subnets.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

Subnets preserve eventual properties and every limit of a net

Statement

If y is a subnet of a net x, then every subset in which x is eventually contained is one in which y is eventually contained. Consequently every limit of x is a limit of y.

Facts & Assumptions

Given: A subnet ye=xϕ(e) of xd.

[A1]

Eventual cofinality says that for every d0∈D some e0∈E has e≥e0⇒ϕ(e)≥d0 (Subnet via an eventually cofinal index map).

[A2]

A net converges to p exactly when it is eventually in every neighbourhood of p (Convergence and cluster points of a net in a topological space).

Proof

technique · direct
1.1

Suppose x is eventually in S⊆X, and choose d0 such that d≥d0 implies xd∈S.

given
2.1

Choose e0 from [A1] for this d0; then e≥e0 gives ye=xϕ(e)∈S. Thus y is eventually in S.

step 1.1A1
3.1

If x converges to p, apply step 2.1 to each neighbourhood of p using [A2]; then y is eventually in every such neighbourhood and converges to p.

step 2.1A2∎
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

A point is a cluster point of a net if and only if some subnet converges to it

Statement

For a net x:D→X and p∈X, p is a cluster point of x if and only if x has a subnet converging to p.

Facts & Assumptions

Given: A net x:D→X in a topological space and a point p∈X.

[A1]

A cluster point is one for which every neighbourhood is visited frequently, and convergence means eventual membership in every neighbourhood (Convergence and cluster points of a net in a topological space).

[A2]

Intersections of finitely many neighbourhoods of p are neighbourhoods of p (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open).

[A3]

A subnet is given by an eventually cofinal index map (Subnet via an eventually cofinal index map).

Proof

technique · constructive
1.1

Suppose p is a cluster point. Let E={(d,N):N∈N(p), d∈D, xd∈N}, ordered by (d,N)⪯(e,M) when d≤e and M⊆N.

A1construct
1.2

Conversely, suppose a subnet ye=xϕ(e) converges to p. Given a neighbourhood N and d∈D, choose e0 after which y lies in N and choose e1 after which ϕ(e)≥d; a common upper bound e of e0,e1 gives ϕ(e)≥d and xϕ(e)=ye∈N. Hence x is frequently in N.

A1A3
2.1

The set E is directed: for (d,N),(e,M)∈E, take h≥d,e in D; frequent membership in N∩M gives k≥h with xk∈N∩M, and (k,N∩M) is above both pairs.

step 1.1A1A2
2.2

Put y(d,N)=xd and ϕ(d,N)=d. For every d0∈D, the pair (d0,X) lies in E, and every later pair has first coordinate at least d0. Thus ϕ is eventually cofinal and y is a subnet of x.

step 1.1A3
2.3

For a neighbourhood N of p, choose (d,N)∈E using frequent membership in N. Every pair later than it has second coordinate contained in N, hence its y-value lies in N. Thus y→p.

step 1.1A1
3.1

Steps 1.1 and 2.1--2.3 construct a convergent subnet from a cluster point, and step 1.2 gives the converse.

step 2.2step 2.3step 1.2discharge-construct∎
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

A point lies in the closure of a set if and only if a net in the set converges to it

Statement

For A⊆X and p∈X, one has p∈A‾ if and only if there is a net in A converging to p.

Facts & Assumptions

Given: A subset A of a topological space X and a point p∈X.

[L3]

A net converges exactly when it is eventually in every neighbourhood (Convergence and cluster points of a net in a topological space).

Proof

technique · constructive
1.1

Suppose p∈A‾. Let E={(N,a):N∈N(p), a∈N∩A}, ordered by (N,a)⪯(M,b) when M⊆N, and put x(N,a)=a.

L1construct
1.2

Conversely, if a net x in A converges to p, every neighbourhood N of p contains some eventual value xd∈A, so N∩A≠∅ and p∈A‾.

L1L3
2.1

The index set is directed: for (N,a),(M,b), the set N∩M is a neighbourhood and meets A; for c∈(N∩M)∩A, the pair (N∩M,c) is above both.

step 1.1L1L2
2.2

Given a neighbourhood N of p, choose (N,a)∈E. Every later pair has its second coordinate in a subset of N, so x is eventually in N and therefore converges to p.

step 1.1L3
3.1

Steps 1.1--2.1 construct the required net and step 1.2 proves the converse.

step 2.2step 1.2discharge-construct∎
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

A map of topological spaces is continuous at a point if and only if it preserves every net converging to that point

Statement

Let f:X→Y and p∈X. Then f is continuous at p if and only if, for every net xd→p in X, the net f(xd) converges to f(p) in Y.

Facts & Assumptions

Given: A function f:X→Y and a point p∈X.

[A1]

f is continuous at p exactly when every neighbourhood V of f(p) has f−1[V] as a neighbourhood of p (Continuity of a map of topological spaces at a point and globally).

[A2]

A point is in the closure of a set exactly when a net in that set converges to it (A point lies in the closure of a set if and only if a net in the set converges to it).

[A3]

A net converges exactly when it is eventually in every neighbourhood (Convergence and cluster points of a net in a topological space).

Proof

technique · contradiction
1.1

If f is continuous at p and xd→p, then for every neighbourhood V of f(p) the net is eventually in f−1[V] by [A1], hence f(xd) is eventually in V and converges to f(p).

A1A3
1.2

Conversely, assume every net converging to p has image converging to f(p), and assume for a contradiction that f is not continuous at p. Then some neighbourhood V of f(p) has f−1[V] not a neighbourhood of p.

A1assume-contra
2.1

Put A=X∖f−1[V]. Every neighbourhood of p meets A, for otherwise it would be contained in f−1[V]; hence p∈A‾ and [A2] gives a net xd in A converging to p.

step 1.2A2
3.1

Every f(xd) lies outside V, so its image net is not eventually in the neighbourhood V of f(p) and cannot converge to f(p), contradicting the assumption of step 1.2.

step 2.1A3
4.1

Therefore f is continuous at p; together with step 1.1 this proves the equivalence.

step 1.1step 3.1discharge-contradiction∎
TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

A topological space is Hausdorff if and only if every net has at most one limit

Statement

A topological space X is Hausdorff if and only if every net in X has at most one limit.

Facts & Assumptions

Given: A topological space X.

[A2]

A net converges to a point exactly when it is eventually in each of that point's neighbourhoods (Convergence and cluster points of a net in a topological space).

Proof

technique · constructive
1.1

Suppose X is Hausdorff and a net converges to both p and q. If p≠q, take disjoint neighbourhoods U of p and V of q; the net is eventually in both, and directedness supplies an index after both thresholds, whose value would lie in U∩V.

A1A2
1.2

Conversely, suppose X is not Hausdorff. Choose distinct p,q for which every neighbourhood of p meets every neighbourhood of q, and let E={(U,V,z):U∈N(p), V∈N(q), z∈U∩V}, ordered by reverse inclusion in the first two coordinates.

A1construct
2.1

Thus p=q, so every net has at most one limit.

step 1.1
2.2

The set E is directed: intersect the first two neighbourhood coordinates of two triples and choose a point in their intersection; the resulting triple is above both. The net sending (U,V,z) to z is eventually in every neighbourhood of p and every neighbourhood of q, hence converges to both distinct points.

step 1.2A1A2
3.1

Therefore uniqueness of all net limits forces X to be Hausdorff, and the two implications prove the result.

step 2.1step 2.2discharge-construct∎
DefinitionDefinition: AI-adaptedProof: AI-generatedjudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

The tail filter of a net

Definition

For a net x:D→X, put Td={xe:d≤e} and Bx={Td:d∈D}. This is a filter base: it is nonempty, each Td contains xd, and if f≥d,e then Tf⊆Td∩Te. Its generated filter The upward closure of a filter base is the smallest filter containing it is the tail filter of x:

Fx={A⊆X:some d∈D has Td⊆A}.

Thus A∈Fx exactly when the net is eventually in A. The preceding filter-base verification makes this a well-defined filter in the sense of Filter on a set.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

Convergence and cluster points of a filter on a topological space

Definition

Let F be a filter on a topological space X and let p∈X.

  • F converges to p, written F→p, if every neighbourhood of p belongs to F.
  • p is a cluster point of F if N∩A≠∅ for every neighbourhood N of p and every A∈F.

The second condition says precisely that the neighbourhood filter at p and F have no disjoint members.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

A net and its tail filter have the same limits and cluster points

Statement

For a net x and its tail filter Fx, a point is a limit of x exactly when it is a limit of Fx, and it is a cluster point of x exactly when it is a cluster point of Fx.

Facts & Assumptions

Given: A net x:D→X, its tail filter Fx, and p∈X.

[A1]

A∈Fx exactly when x is eventually in A (The tail filter of a net).

[A2]

Net and filter convergence and cluster points have their stated neighbourhood formulations (Convergence and cluster points of a net in a topological space, Convergence and cluster points of a filter on a topological space).

Proof

technique · direct
1.1

For every neighbourhood N of p, x is eventually in N exactly when N∈Fx by [A1]. Thus the two convergence conditions in [A2] are equivalent.

A1A2
1.2

For every neighbourhood N of p, x is frequently in N exactly when N meets every tail Td: a point in N∩Td is a value xe∈N with e≥d.

A1A2
2.1

If N meets every tail, it meets every member of Fx, since each such member contains a tail; conversely every tail belongs to Fx. Hence the two cluster-point conditions in [A2] are equivalent.

step 1.2A1A2∎
DefinitionDefinition: AI-adaptedProof: AI-generatedjudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

The canonical net indexed by the pairs (A,x) with A in a filter and x∈A

Definition

Let F be a filter on X. Its derived-net index set is

EF={(A,x):A∈F, x∈A},

ordered by (A,x)⪯(B,y) when B⊆A. It is a directed preorder: filters contain no empty set, and for two indices choose z∈A∩B, so (A∩B,z) is above both. The net derived from F is

x(A,x):=x((A,x)∈EF).

This construction makes no arbitrary choice, because the point x is included in the index.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

A filter and its canonical derived net have the same limits and cluster points

Statement

A filter F and the net derived from it have exactly the same limits and cluster points.

Facts & Assumptions

Given: A filter F on X, its derived net, and p∈X.

[A1]

The derived net is indexed by (A,x) with A∈F, x∈A, ordered by reverse inclusion of the first coordinate (The canonical net indexed by the pairs (A,x) with A in a filter and x∈A).

[A2]

Filter and net convergence and cluster points have their stated neighbourhood formulations (Convergence and cluster points of a filter on a topological space, Convergence and cluster points of a net in a topological space).

Proof

technique · direct
1.1

If a neighbourhood N of p belongs to F, choose x∈N; then (N,x) is an index, and every later (B,y) has B⊆N, hence y∈N. Thus filter convergence implies convergence of the derived net.

A1A2
2.1

If the derived net is eventually in N, take a threshold (A,x). Applying eventuality to indices (A,y) with y∈A gives A⊆N; upward closure of the filter gives N∈F. Thus convergence is equivalent.

step 1.1A1A2
3.1

The derived net is frequently in N exactly when every A∈F meets N: after (A,x) a point of A∩N supplies a later index, and conversely frequent membership after (A,x) supplies such a point. Therefore its cluster points are exactly those of F.

A1A2∎
TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

The tail-filter and derived-net constructions preserve convergence and cluster points in both directions

Statement

Passing from a net to its tail filter, or from a filter to its derived net, preserves and reflects convergence and cluster points.

Facts & Assumptions

Given: A net, a filter, and a point of the relevant topological space.

[L1]

A net and its tail filter have the same limits and cluster points (A net and its tail filter have the same limits and cluster points).

[L2]

A filter and its derived net have the same limits and cluster points (A filter and its canonical derived net have the same limits and cluster points).

Proof

technique · direct
1.1

Apply [L1] to the given net.

L1
1.2

Apply [L2] to the given filter.

L2
2.1

These are precisely the two asserted correspondences.

step 1.1step 1.2∎
DefinitionDefinition: Literature-sourcedProof: AI-generatedjudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

Universal net: eventually in every subset or eventually in its complement

Definition

A net x:D→X is universal if, for every subset S⊆X, it is eventually in S or eventually in X∖S.

The two alternatives cannot both occur: directedness would give an index after both thresholds, whose value would belong to the empty intersection S∩(X∖S).

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

A net is universal exactly when its tail filter is an ultrafilter, and the canonical net of an ultrafilter is universal

Statement

A net is universal if and only if its tail filter is an ultrafilter. Moreover, the net derived from an ultrafilter is universal.

Facts & Assumptions

Given: A net x in X and a filter U on X.

[A1]

S belongs to the tail filter of x exactly when x is eventually in S (The tail filter of a net).

[A2]

A filter is an ultrafilter exactly when, for every S⊆X, it contains S or X∖S (Characterisation of ultrafilters: every set or its complement).

[A3]

The derived net of U is indexed by (A,a) and later indices have first coordinate contained in A (The canonical net indexed by the pairs (A,x) with A in a filter and x∈A).

Proof

technique · direct
1.1

By [A1], universality of x says exactly that its tail filter contains S or X∖S for every S⊆X. By [A2], this is exactly ultrafilterhood.

A1A2
1.2

If U is an ultrafilter and S⊆X, [A2] gives S∈U or X∖S∈U. In the first case an index (S,a) exists and every later value lies in S by [A3]; the second case is identical.

A2A3
2.1

Thus the derived net of an ultrafilter is universal, completing both assertions.

step 1.1step 1.2∎
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

Every cluster point of an ultrafilter is a limit of that ultrafilter

Statement

Every cluster point of an ultrafilter is a limit of that ultrafilter.

Facts & Assumptions

Given: An ultrafilter U on X and a cluster point p of it.

[A1]

U→p means every neighbourhood of p belongs to U, while clusterhood means every such neighbourhood meets every member of U (Convergence and cluster points of a filter on a topological space).

[A2]

For every subset S, an ultrafilter contains S or its complement (Characterisation of ultrafilters: every set or its complement).

Proof

technique · contradiction
1.1

Assume for a contradiction that U does not converge to p. Then some neighbourhood N of p is not in U.

A1assume-contra
2.1

By [A2], X∖N∈U. But N must meet every member of U by clusterhood, whereas N∩(X∖N)=∅.

step 1.1A1A2
3.1

This contradiction proves U→p.

step 2.1discharge-contradiction∎
TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

Assuming the ultrafilter lemma, compactness is equivalent to every net having a cluster point, every net having a convergent subnet, every filter having a cluster point, and every ultrafilter converging

Statement

Assume the ultrafilter lemma. For a topological space X, the following are equivalent:

  1. X is compact;
  2. every net in X has a cluster point;
  3. every net in X has a convergent subnet;
  4. every filter on X has a cluster point;
  5. every ultrafilter on X converges.

Facts & Assumptions

Given: A topological space X and the ultrafilter lemma.

[L1]

Compactness is equivalent to every family of closed sets with the finite-intersection property having nonempty intersection; moreover, a family of subsets of X has the finite-intersection property exactly when it is contained in a filter on X (A space is compact exactly when every family of closed subsets with the finite intersection property has nonempty intersection, clauses 1 and 2).

[L2]

A net has p as a cluster point exactly when it has a subnet converging to p (A point is a cluster point of a net if and only if some subnet converges to it).

[L3]

A net and its tail filter have the same cluster points, and a filter and its derived net have the same cluster points (The tail-filter and derived-net constructions preserve convergence and cluster points in both directions).

[L4]

Proof

technique · direct
1.1

Suppose X is compact and F is a filter. The closed family {A‾:A∈F} has the finite-intersection property, because a finite intersection of members of F is nonempty and is contained in the corresponding intersection of closures. By [L1], choose p∈⋂A∈FA‾.

L1
1.2

If every filter has a cluster point, apply this to a net's tail filter and use [L3]; hence 4 implies 2. By [L2], conditions 2 and 3 are equivalent.

L2L3
1.3

Conversely, if every net has a cluster point and F is a filter, its derived net has a cluster point, which is also a cluster point of F by [L3]. Hence 2 implies 4.

L3
1.4

Condition 4 implies 5 because an ultrafilter is a filter and [L4] turns its cluster point into a limit.

L4
1.5

Suppose every ultrafilter converges and let C be a family of closed subsets of X with the finite-intersection property. Clause 2 of [L1] gives a filter containing C, and [L4] extends it to an ultrafilter U.

L1L4
2.1

Every neighbourhood of p meets every A∈F, since p∈A‾; thus p is a cluster point of F. Hence 1 implies 4.

step 1.1L1
2.2

Let p be a limit of U. For C∈C, every neighbourhood of p belongs to U and meets C∈U; therefore p∈C‾=C. Thus ⋂C≠∅, and [L1] gives compactness.

step 1.5L1
3.1

The implications in steps 2.1, 1.2, 1.3, 1.4 and 2.2 establish all five equivalences.

step 2.1step 1.2step 1.3step 1.4step 2.2∎
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

Every cluster point of a universal net is a limit of that net

Statement

Every cluster point of a universal net is a limit of that net.

Facts & Assumptions

Given: A universal net x:D→X and a cluster point p.

[A1]

A universal net is eventually in S or eventually in X∖S for every subset S (Universal net: eventually in every subset or eventually in its complement).

[A2]

Clusterhood is frequent membership in every neighbourhood, while convergence is eventual membership in every neighbourhood (Convergence and cluster points of a net in a topological space).

Proof

technique · contradiction
1.1

Assume for a contradiction that x does not converge to p. Then some neighbourhood N of p is not an eventual set for x.

A2assume-contra
2.1

By universality, x is eventually in X∖N. This contradicts frequent membership in N, since an index after both thresholds would lie in N∩(X∖N).

step 1.1A1A2
3.1

Therefore x converges to p.

step 2.1discharge-contradiction∎
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

The image of a universal net under any map is universal, and a continuous map preserves its limits

Statement

If x is a universal net in X and f:X→Y is any map, then f(x) is universal. If f is continuous and x→p, then f(x)→f(p).

Facts & Assumptions

Given: A universal net x:D→X and a map f:X→Y.

[A1]

x is universal precisely when it eventually enters every subset or its complement (Universal net: eventually in every subset or eventually in its complement).

Proof

technique · direct
1.1

Let S⊆Y. By [A1], x is eventually in f−1[S] or in its complement f−1[Y∖S]; respectively, f(x) is eventually in S or in Y∖S.

A1
2.1

Thus f(x) is universal.

step 1.1A1
3.1

If f is continuous and x→p, the second assertion is [L1].

L1∎
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

Assuming the ultrafilter lemma, every net has a universal subnet

Statement

Assume the ultrafilter lemma. Every net has a universal subnet.

Facts & Assumptions

Given: A net x:D→X and its tail filter Fx.

[A1]

Fx contains every tail Td, and its members contain a tail (The tail filter of a net).

[L1]

The ultrafilter lemma extends Fx to an ultrafilter U (The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter).

[L2]

An ultrafilter contains every subset or its complement (Characterisation of ultrafilters: every set or its complement).

[A2]

A subnet uses an eventually cofinal index map (Subnet via an eventually cofinal index map).

[A3]

A universal net is eventually in every set or its complement (Universal net: eventually in every subset or eventually in its complement).

Proof

technique · constructive
1.1

Choose an ultrafilter U⊇Fx by [L1]. Let E={(d,A):d∈D, A∈U, xd∈A}, ordered by (d,A)⪯(e,B) when d≤e and B⊆A, and put y(d,A)=xd.

L1construct
2.1

The set E is directed. Given (d,A),(e,B), choose h≥d,e. Since A∩B and the tail Th belong to U, their intersection is nonempty; choose an index k≥h with xk∈A∩B. Then (k,A∩B) is above both pairs.

step 1.1A1choose
2.2

The map ϕ(d,A)=d is eventually cofinal: (d0,X) is an index for every d0, and every later index has first coordinate at least d0. Thus y is a subnet of x.

step 1.1A2
2.3

For S⊆X, [L2] gives S∈U or X∖S∈U. In the first case choose any d0∈D. Since S∩Td0∈U, choose j≥d0 with xj∈S. Then (j,S)∈E, and every later value lies in S. The complementary case is identical. Thus y is universal.

step 1.1A1A3L2choose
3.1

The constructed y is a universal subnet of x.

step 2.2step 2.3discharge-construct∎
CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

Assuming the ultrafilter lemma, a space is compact if and only if every universal net converges

Statement

Assume the ultrafilter lemma. A topological space is compact if and only if every universal net in it converges.

Facts & Assumptions

Given: A topological space X and the ultrafilter lemma.

[L2]

Every net has a universal subnet (Assuming the ultrafilter lemma, every net has a universal subnet), and a cluster point of a universal net is a limit (Every cluster point of a universal net is a limit of that net).

[L3]

A point is a cluster point of a net exactly when some subnet converges to it (A point is a cluster point of a net if and only if some subnet converges to it).

Proof

technique · direct
1.1

If X is compact, a universal net has a cluster point by [L1], hence converges by [L2].

L1L2
1.2

Conversely, suppose every universal net converges. Every net has a universal subnet by [L2], which then converges; its limit is a cluster point of the original net by [L3]. Thus every net has a cluster point.

L2L3
2.1

By [L1], this makes X compact.

step 1.2L1∎
TheoremStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-05 (claude-sonnet-5)Open item page →

Assuming the ultrafilter lemma, an arbitrary product of compact Hausdorff spaces is compact

Statement

Assume the ultrafilter lemma. If (Xi)i∈I is any family of compact Hausdorff spaces, then ∏i∈IXi, with its product topology, is compact.

Facts & Assumptions

Given: Compact Hausdorff spaces Xi, their product P, and a universal net xd in P.

[L2]

Assuming the ultrafilter lemma, a space is compact if and only if every universal net in it converges (Assuming the ultrafilter lemma, a space is compact if and only if every universal net converges).

[L3]

Proof

technique · constructive
1.1

For every i∈I, the projection πi is continuous, so πi(xd) is universal by [L1] and converges in compact Xi by [L2]. Its limit pi is unique by [L3].

L1L2L3
2.1

The uniqueness in step 1.1 defines a point p∈∏i∈IXi, namely the function i↦pi, rather than choosing a family of limits.

step 1.1L3construct
2.2

Let N be a neighbourhood of p in P. By [L4], it contains a basic product neighbourhood restricting a finite set J⊆I; for each i∈J, the coordinate net is eventually in its prescribed neighbourhood of pi. Directedness supplies one index after the finitely many thresholds, and after it xd∈N. Thus xd→p.

step 1.1L4
3.1

Every universal net in P converges by step 2.2. The converse direction of [L2] therefore makes P compact.

step 2.2L2discharge-construct∎
RemarkRemark: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

The compact Hausdorff product theorem uses the ultrafilter lemma, while the published arbitrary compact product theorem assumes the full Axiom of Choice

The proof of Assuming the ultrafilter lemma, an arbitrary product of compact Hausdorff spaces is compact spends the ultrafilter lemma at the universal-subnet step. The published Tychonoff's theorem: an arbitrary product of compact spaces is compact in the product topology, assuming the Axiom of Choice asserts compactness for arbitrary compact factors under the full Axiom of Choice (The Axiom of Choice). These are distinct stated hypotheses; this page makes no claim about their exact relative strength.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

Fréchet–Urysohn spaces and sequential spaces

Definition

A topological space X is Fréchet–Urysohn if, whenever p∈A‾, there is a sequence in A converging to p. Equivalently, seqcl⁡(A)=A‾ for every A⊆X, since sequential closure is always contained in closure (The sequential closure is contained in the closure, continuity implies sequential continuity, and sequential limits need not be unique).

A subset C⊆X is sequentially closed if every sequence in C that converges in X has its limit in C. The space is sequential if every sequentially closed subset is closed. Equivalently, seqcl⁡(A)=A implies A‾=A for every A⊆X.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

Assuming countable choice, every first countable space is Fréchet–Urysohn; in ZF every Fréchet–Urysohn space is sequential

Statement

Assume countable choice. Every first countable space is Fréchet–Urysohn. In ZF, every Fréchet–Urysohn space is sequential.

Facts & Assumptions

Given: A topological space X.

[A1]

A space is Fréchet--Urysohn when seqcl⁡(A)=A‾ for every subset A, and it is sequential when every sequentially closed subset is closed (Fréchet–Urysohn spaces and sequential spaces).

Proof

technique · direct
1.1

Under countable choice, [L1] is exactly the defining equality for a first countable space to be Fréchet–Urysohn.

L1A1
1.2

Now suppose X is Fréchet–Urysohn and C is sequentially closed. Then seqcl⁡(C)=C, because the constant sequence gives C⊆seqcl⁡(C) and sequential closedness gives the reverse inclusion.

L2
2.1

Fréchet–Urysohnness gives C‾=seqcl⁡(C)=C, so C is closed. Therefore X is sequential.

step 1.2A1∎

5 · Examples, counterexamples and false statements

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31Open item page →

FALSE: every subnet of a sequence is a subsequence

Statement

FALSE. Every subnet of a sequence is a subsequence.

Facts & Assumptions

Given: The discrete topological space N and its identity sequence xn=n.

[A1]

A subnet may use any eventually cofinal index map; it need not use a strictly increasing map (Subnet via an eventually cofinal index map).

[A2]

A subsequence of x is a composite x∘h with h:N→N strictly increasing; such an h is injective (A strictly increasing index map satisfies nk≥k).

Refutation

technique · direct
1.1

Put ϕ(0)=0 and ϕ(k)=k−1 for k≥1, and let yk=xϕ(k). For every n, all k≥n+1 satisfy ϕ(k)=k−1≥n, so ϕ is eventually cofinal and y is a subnet of x.

A1
2.1

The subnet has y0=y1=0. Every subsequence of the injective identity sequence is injective by [A2], so y cannot be a subsequence of x.

step 1.1A2
3.1

Thus the stated universal claim is false.

step 2.1∎

Sources