theorem
PiBase.Homeomorph.nontrivial
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[Nontrivial X]
(f : X ≃ₜ Y)
:
theorem
PiBase.WellDefined.nontrivial :
WellDefined fun (X : Type u_3) [TopologicalSpace X] => Nontrivial X