Theorem IsClosed.mk_lt_two_pow_mk_dense

Modification history

2026-01-06 20:52

Mathlib/Topology/Separation/NotNormal.lean

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

Added IsClosed.mk_lt_two_pow_mk_dense View on Github →