mathlib3 documentation

topology.algebra.order.t5

Linear order is a completely normal Hausdorff topological space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.