Theorems · Theorem · general topology

closure_Ico

∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α},
  a ≠ b → closure (Set.Ico a b) = Set.Icc a b

The closure of the interval [a, b) is the closed interval [a, b].

Defined in

Mathlib.Topology.Order.DenselyOrdered

Cited by

4 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderOrderTopologyDenselyOrdered