Commit 2023-12-16 06:46 4ded391b

View on Github →

feat: A finite topological space is second countable (#8955) From PFR

Estimated changes

Modified Mathlib/Topology/Bases.lean

Modified Mathlib/Topology/Clopen.lean

modified theorem isClopen_empty

modified theorem isClopen_univ