Metrization
The Nagata–Smirnov sigma-locally-finite open-basis criterion and its metric converse, and metrizability from a locally finite closed metrizable neighbourhood cover, preserving the given topologies.
Quoted from the project description in formalization.yaml of FormalFrontier/metrization at commit 9c7cf0d8, Apache-2.0.
3 articles: 3 for headline results in its README whose declaration link names a declaration the scan finds in the linked file.
Facts
From the repository and its formalization.yaml; the review and automation statements are quoted as written.
- Repository: FormalFrontier/metrization, read at commit 9c7cf0d8 (2026-11-04).
- Lean toolchain v4.34.0-rc2, Mathlib at 83abb3e7.
- License: Apache-2.0.
- Authors: Formal Frontier Agents.
- Review status: “agent-reviewed”.
- Automation: agent; tool setup “Lean 4 and Mathlib”
- Automation notes: “AI agents contributed to the formalization and documentation.”
Literature
The sources its formalization.yaml names, with their relationship to it.
- On a necessary and sufficient condition of metrizability, J. Nagata, The sigma-locally-finite basis criterion for metrizability (article; adapts).
- A necessary and sufficient condition for metrizability of a topological space, Yu. M. Smirnov, The sigma-locally-finite basis criterion for metrizability (article; adapts).
- Mathlib, The Mathlib Community, Topological bases, locally finite families, separation and Urysohn's lemma, metric paracompactness, countable products, finite-support Lp metrics and coproduct homeomorphisms (software; adapts).
Builds on
No other Formal Frontier library.
Used by
Headline results
Quoted from the headline results in README.md of FormalFrontier/metrization at commit 9c7cf0d8, Apache-2.0.
TheoremSigma-locally-finite basis criterion#
A T₃ space is metrizable if it has an open basis in countably many locally finite indexed levels. Each level may have an arbitrary index type; local finiteness counts the original indices, including repetitions.
Quoted from the headline results in README.md of FormalFrontier/metrization at commit 9c7cf0d8, Apache-2.0.
Lean
TopologicalSpace.metrizableSpace_of_sigmaLocallyFinite_isTopologicalBasis(theorem), declared in Metrization/LocallyFinite.lean, line 48.
Read from the source at commit 9c7cf0d8, without running Lean.
Sources
TheoremMetric converse#
Every metrizable space has an open basis in countably many locally finite levels, each indexed by the points of the space.
Quoted from the headline results in README.md of FormalFrontier/metrization at commit 9c7cf0d8, Apache-2.0.
Lean
TopologicalSpace.exists_sigmaLocallyFinite_isTopologicalBasis(theorem), declared in Metrization/LocallyFinite.lean, line 149.
Read from the source at commit 9c7cf0d8, without running Lean.
Sources
TheoremClosed metrizable neighbourhood-cover criterion#
A space is metrizable if it has a locally finite family of closed subsets whose interiors cover the space and each of which is metrizable in its original subtype topology. No ambient separation assumption is required.
Quoted from the headline results in README.md of FormalFrontier/metrization at commit 9c7cf0d8, Apache-2.0.
Lean
TopologicalSpace.metrizableSpace_of_locallyFinite_isClosed_interior_cover(theorem), declared in Metrization/LocallyFinite.lean, line 189.
Read from the source at commit 9c7cf0d8, without running Lean.
Sources
Main results
Its formalization.yaml lists 3 main results, and the scan finds 3 of them declared in the file the yaml gives; they are on their own page, not made articles.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.