Theorem IsClosed.two_pow_mk_le_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.two_pow_mk_le_two_pow_mk_dense View on Github →