instance
PiBase.instLotsOfOrderTopology
{X : Type u_3}
[TopologicalSpace X]
[h : LinearOrder X]
[h' : OrderTopology X]
:
Lots X
theorem
PiBase.Homeomorph.lots
{X : Type u_3}
{Y : Type u_4}
[TopologicalSpace X]
[TopologicalSpace Y]
[h : Lots X]
(f : X ≃ₜ Y)
:
Lots Y
The order topology transported along a homeomorphism is again an order topology.