Main results
The main results that the formalization.yaml of FormalFrontier/metrization lists under status.main_results at commit 9c7cf0d8, each that the scan finds declared in the file the yaml gives, with its line. They are listed here, not made articles: in several Formal Frontier libraries this list is close to the whole API. The notes are the yaml's.
| Declaration | Kind | Where | Note |
|---|---|---|---|
TopologicalSpace.metrizableSpace_of_sigmaLocallyFinite_isTopologicalBasis |
theorem | Metrization/LocallyFinite.lean, line 48 | |
TopologicalSpace.exists_sigmaLocallyFinite_isTopologicalBasis |
theorem | Metrization/LocallyFinite.lean, line 149 | |
TopologicalSpace.metrizableSpace_of_locallyFinite_isClosed_interior_cover |
theorem | Metrization/LocallyFinite.lean, line 189 |
Quoted from the main results in formalization.yaml of FormalFrontier/metrization at commit 9c7cf0d8, Apache-2.0.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.