Perfectly normal topological spaces.

This file proves some properties of a perfectly normal space.

TODO

Prove that the product of a perfectly normal space and a metric space is perfectly normal.

theorem perfectlyNormalSpace_iff_forall_isClosed_preimage_zero {X : Type u_1} [TopologicalSpace X] : PerfectlyNormalSpace X ↔ ∀ (s : Set X), IsClosed s → ∃ (f : C(X, ℝ)), 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.

@[deprecated Topology.IsInducing.perfectlyNormalSpace (since := "2026-06-03")]

theorem Topology.IsEmbedding.perfectlyNormalSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [PerfectlyNormalSpace Y] {e : X → Y} (he : IsInducing e) : PerfectlyNormalSpace X

Alias of Topology.IsInducing.perfectlyNormalSpace.