Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-10 01:42 f7d03fec

View on Github →

feat(counterexamples/sorgenfrey_line): new file (#14820) Define the Sorgenfrey line and prove that it is a normal topological space but its product with itself is not a normal topological space.

Estimated changes