Theorems · Theorem · general topology

dense_iff_exists_between

∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] [Nontrivial α]
  {s : Set α}, Dense s ↔ ∀ (a b : α), a < b → ∃ c ∈ s, a < c ∧ c < b

A set in a nontrivial densely linear ordered type is dense in the sense of topology if and only if for any a < b there exists c ∈ s, a < c < b. Each implication requires less typeclass assumptions.

Defined in

Mathlib.Topology.Order.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderOrderTopologyDenselyOrderedNontrivial