Alphabeta Math

Convergence: Nets and Filters

About this page
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.
1 · Prerequisites
Real Analysis
Set Theory
Topology
2 · Logical flowchart

3 · Items

Definition

Directed preorders and nets

Definition

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

Definition

Convergence and cluster points of a net in a topological space

Definition

Subnet via an eventually cofinal index map

Lemma

Subnets preserve eventual properties and every limit of a net

Theorem

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

Theorem

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

Theorem

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

Theorem

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

Definition

The tail filter of a net

Definition

Convergence and cluster points of a filter on a topological space

Lemma

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

Definition

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

Lemma

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

Theorem

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

Definition

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

Theorem

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

Lemma

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

Theorem

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

Lemma

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

Lemma

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

Lemma

Assuming the ultrafilter lemma, every net has a universal subnet

Corollary

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

Theorem

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

Remark

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

Definition

Fréchet–Urysohn spaces and sequential spaces

Theorem

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

False statement

FALSE: every subnet of a sequence is a subsequence

Sources