Theorems · Theorem · general topology

IsClosed.two_pow_mk_le_two_pow_mk_dense

∀ {X : Type u} [inst : TopologicalSpace X] [NormalSpace X] {s d : Set X},
  IsClosed s → ∀ [DiscreteTopology ↑s], Dense d → 2 ^ Cardinal.mk ↑s ≤ 2 ^ Cardinal.mk ↑d

Let s be a closed set in a normal space and d be a dense set. If the induced topology on s is discrete, then 𝒫 s has cardinality less than or equal to 𝒫 d.

Defined in

Mathlib.Topology.Separation.NotNormal

Cited by

2 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceNormalSpaceDiscreteTopology