Order topology on WithTop ι #
When ι is a topological space with the order topology, we also endow WithTop ι with the order
topology. If ι is second countable, we prove that WithTop ι also is.
instance
TopologicalSpace.instWithTopOfOrderTopology
{ι : Type u_1}
[Preorder ι]
[TopologicalSpace ι]
[OrderTopology ι]
:
instance
TopologicalSpace.instOrderTopologyWithTop
{ι : Type u_1}
[Preorder ι]
[TopologicalSpace ι]
[OrderTopology ι]
:
OrderTopology (WithTop ι)
instance
TopologicalSpace.instSecondCountableTopologyWithTop
{ι : Type u_1}
[Preorder ι]
[ts : TopologicalSpace ι]
[ht : OrderTopology ι]
[SecondCountableTopology ι]
: