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

theorem PiBase.WellDefined.countablyInfinite : WellDefined fun (X : Type u_1) [TopologicalSpace X] => CountablyInfinite X