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

theorem PiBase.WellDefined.cardLePowerContinuum : WellDefined fun (X : Type u) [TopologicalSpace X] => CardLePowerContinuum X