mathlib3

f7d03fec - feat(counterexamples/sorgenfrey_line): new file (#14820)

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.