theorem
PiBase.Homeomorph.cardGeThree
{X : Type u}
{Y : Type v}
[TopologicalSpace X]
[TopologicalSpace Y]
[h : CardGeThree X]
(f : X ≃ₜ Y)
:
theorem
PiBase.WellDefined.cardGeThree :
WellDefined fun (X : Type u_1) [TopologicalSpace X] => CardGeThree X