mathlib documentation

topology.algebra.order.t5

Linear order is a completely normal Hausdorff topological space #

In this file we prove that a linear order with order topology is a completely normal Hausdorff topological space.

@[protected, instance]

A linear order with order topology is a completely normal Hausdorff topological space.