Mathlib Map

Map · 54

general topology

MSC 54 · General topology

22,030 declarations (18,559 theorems, 3,471 definitions) across 456 files. 7 of the 30 famous theorems listed for this area are in Mathlib (23%), 8 in some Lean library. 14 open conjectures here are stated in Lean.

Files are assigned to areas by a language model reading each file's documentation. Report a file that is in the wrong area.

Subareas7

  • 54A Generalities in topology 5,834
  • 54E Topological spaces with richer structures 5,570
  • 54C Maps and general types of topological spaces defined by maps 3,764
  • 54D Fairly general properties of topological spaces 3,476
  • 54B Basic constructions in general topology 1,267
  • 54H Connections of general topology with other structures, applications 1,097
  • 54F Special properties of topological spaces 1,022

Famous theorems7 of 30

From the 1000+ theorems project, which classifies each theorem by MSC area.

Not yet in Mathlib · 23

In Mathlib · 7

From the 100 theorems list1

Open conjectures stated in Lean14

Statements without proofs, collected by the Formal Conjectures project.

Undergraduate topics still missing3 of 44

From Mathlib's own undergraduate checklist.

Topology · 3 of 44

  • Normed vector spaces on $\R$ and $\C$ › equivalent norms
  • Hilbert spaces › example, classical Hilbert bases of orthogonal polynomials
  • Hilbert spaces › $H^1_0([0,1])$ and its application to the one-dimensional Dirichlet problem

Structures defined here24

Typeclasses defined in this area's files, most assumed first.

Files456

Largest first. The code after each file is its assigned subarea.