Linear upper or lower sets topologies are completely normal #
@[instance 100]
instance
instCompletelyNormalSpaceOfIsUpperSet
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[Topology.IsUpperSet α]
:
@[instance 100]
instance
instCompletelyNormalSpaceOfIsLowerSet
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[Topology.IsLowerSet α]
: