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