Topology · existing Mathlib theorem

Tychonoff's Theorem

For each index i, choose a compact subset s i of a topological space X i. The set of all dependent functions x with x i inside s i for every i is compact in the product topology, even when the index type is infinite.

topological spaces
compact sets
product topology
arbitrary products

Four separate status axes

Upstream indexedPinned source bytes verified locally

Locally reproducedExact upstream declaration replayed

Reviewed pageCurrent public presentation reviewed

Accepted Atlas resultNot recorded for the preferred artifact

These states distinguish upstream identity, local reproduction, review, and Atlas acceptance. This page is part of the public, read-only Mathlib landmark collection.

Formal orientation

Statement map

This deterministic map orients the reader from the mathematical summary to the pinned declaration and exact checked form. The HTML statement below is authoritative.

The theorem at a glance

Tychonoff's Theorem at a glance

A source-bound editorial overview of the exact Mathlib formulation. The image is explanatory; the statement map, formal type, and pinned source remain authoritative.

An ivory theorem poster sends an open-ended index family into indexed topological coordinate spaces, marks one compact subset in each, and gathers the coordinate constraints into a compact dependent product subset. — Compact coordinate subsets over an arbitrary index type form a compact constrained dependent product, with no nonemptiness claim.

An infinite field of enclosed coordinate worlds recedes into the distance while emerald and cobalt threads gather their chosen points into one luminous, enclosed product space. — Compact coordinate spaces combine into a compact product; the receding family suggests an unrestricted index set.

Complementary intuition

A mathematical landmark

Tychonoff's theorem is one of topology's central compactness principles. Its arbitrary-product scope is a decisive reason product topology is defined as it is.

The low-text schematic gives the theorem a visual identity; it does not replace the source-bound poster or exact statement.

Authoritative formal type

Exact Mathlib statement

isCompact_pi_infinite {ι : Type u₁} {X : ι → Type u₂} [(i : ι) → TopologicalSpace (X i)] {s : (i : ι) → Set (X i)} : (∀ i, IsCompact (s i)) → IsCompact {x | ∀ i, x i ∈ s i}

Selected evidence declaration text

theorem isCompact_pi_infinite {ι : Type u₁} {X : ι → Type u₂} [(i : ι) → TopologicalSpace (X i)] {s : (i : ι) → Set (X i)} : (∀ i, IsCompact (s i)) → IsCompact {x | ∀ i, x i ∈ s i}

Proof architecture

How ultrafilter limits prove product compactness

3 curated stages

The checked source rewrites compactness and product convergence in ultrafilter form, maps the ultrafilter through every coordinate evaluation, applies compactness in each factor, and then chooses the coordinate limits and reassembles them into convergence in the product topology.

These source-anchored stages explain the retained Mathlib proof route. They are generated explanations, not proof evidence or an extracted Lean proof-term dependency graph.

Product compactness becomes an ultrafilter convergence problem
Product compactness becomes an ultrafilter convergence problem
Mathlib rewrites compactness, product neighborhoods, and product membership so the proof begins with an ultrafilter containing the constrained product subset.
Open original image in a new tab
Mathlib rewrites compactness, product neighborhoods, and product membership so the proof begins with an ultrafilter containing the constrained product subset.
f <= principal {x | forall i, x i in s i} implies a required product limit
isCompact_iff_ultrafilter_le_nhds, nhds_pi, le_pi, and le_principal_iff transform the compactness goal into a convergence problem for an arbitrary ultrafilter lying over the dependent product subset. This reformulation introduces no coordinate witnesses yet.
Every coordinate projection acquires a compact limit
Every coordinate projection acquires a compact limit
Mapping the ultrafilter through each evaluation map preserves membership in the corresponding compact set, so coordinate compactness provides a limit point there.
Open original image in a new tab
Mapping the ultrafilter through each evaluation map preserves membership in the corresponding compact set, so coordinate compactness provides a limit point there.
exists x, x in s i and Tendsto (Function.eval i) f (nhds x)
For each index i, Mathlib maps the ultrafilter through Function.eval i. Membership of the constrained product implies that the mapped ultrafilter contains s i; compactness of s i then supplies a point x i in that set and convergence of the projected filter to it.
Coordinate limits reassemble into a product limit
Coordinate limits reassemble into a product limit
Dependent choice selects the coordinate limits; their membership and coordinatewise convergence assemble the required point and convergence in the product topology.
Open original image in a new tab
Dependent choice selects the coordinate limits; their membership and coordinatewise convergence assemble the required point and convergence in the product topology.
x i in s i for every i, and Tendsto f (nhds x)
choose x hx using this forms the dependent function from the coordinate witnesses. The membership component of hx i places the resulting function in the constrained product, while the convergence component for every coordinate reassembles through le_pi into convergence to that function in the product topology.

Claim boundary

No new theorem is claimed

The selected Mathlib declaration proves compactness of the dependent product subset {x | ∀ i, x i ∈ s i}. It does not state a finite-product-only result, and the page does not hide the family of topology instances or identify explanatory artwork with proof evidence.

Proof Atlas did not originate Tychonoff's theorem or Mathlib's declaration.
The local evidence checks this exact upstream declaration at one pinned Mathlib commit.
The page does not independently classify the theorem's foundational choice principles beyond the recorded axiom report.

Provenance

Origin and evidence stay separate

Existing declaration: isCompact_pi_infinite in mathlib
Relationship: The checked artifact is the upstream declaration itself
Preferred checked artifact: artifact.library.mathlib.tychonoff-theorem.v001
Source handling: Verified upstream reference; no mirrored source package