Theorems · Theorem · general topology

perfectlyNormalSpace_iff_forall_isClosed_preimage_zero

∀ {X : Type u_1} [inst : TopologicalSpace X],
  PerfectlyNormalSpace X ↔ ∀ (s : Set X), IsClosed s → ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Set.Icc 0 1

A topological space is perfectly normal iff every closed set is the zero set of a continuous function taking values in the unit interval.

Defined in

Mathlib.Topology.Separation.PerfectlyNormal

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpace