theorem PiBase.WellDefined.almostDiscreteSpace : WellDefined AlmostDiscreteSpace

theorem PiBase.Homeomorph.almostDiscreteSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [AlmostDiscreteSpace X] (f : X ≃ₜ Y) : AlmostDiscreteSpace Y