Commit 2026-01-06 20:52 030b1f78

View on Github →

feat(Topology/Separation/NotNormal): generalize to non-separable spaces (#33414)

Estimated changes

Modified Counterexamples/SorgenfreyLine.lean

Modified Mathlib/Topology/Separation/NotNormal.lean

modified theorem IsClosed.mk_lt_continuum

added theorem IsClosed.mk_lt_two_pow_mk_dense

modified theorem IsClosed.not_normal_of_continuum_le_mk

added theorem IsClosed.two_pow_mk_le_two_pow_mk_dense

added theorem IsClosed.two_pow_mk_lt_continuum