Theorems · Theorem · general topology

Dense.Iio_eq_biUnion

∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] [DenselyOrdered α]
  {s : Set α}, Dense s → ∀ (x : α), Set.Iio x = ⋃ y ∈ s ∩ Set.Iio x, Set.Iio y

Defined in

Mathlib.Topology.Order.OrderClosed

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderOrderClosedTopologyDenselyOrdered