Theorems · Theorem · general topology

DiscreteTopology.of_predOrder_succOrder

∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] [PredOrder α] [SuccOrder α],
  DiscreteTopology α

The only order closed topology on a linear order which is a PredOrder and a SuccOrder is the discrete topology. This theorem is not an instance, because it causes searches for PredOrder and SuccOrder with their Preorder arguments and very rarely matches.

Defined in

Mathlib.Topology.Order.OrderClosed

Cited by

1 results in Mathlib

Foundations

Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceLinearOrderOrderClosedTopologyPredOrderSuccOrder