theorem PiBase.WellDefined.fullyNormalSpace : WellDefined FullyNormalSpace

theorem PiBase.Homeomorph.fullyNormalSpace {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [FullyNormalSpace X] (f : X ≃ₜ Y) : FullyNormalSpace Y