Order topology on a densely ordered set #
theorem
closure_Ioi'
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a : α}
(h : (Set.Ioi a).Nonempty)
:
The closure of the interval (a, +∞) is the closed interval [a, +∞), unless a is a top
element.
@[simp]
theorem
closure_Ioi
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
(a : α)
[NoMaxOrder α]
:
The closure of the interval (a, +∞) is the closed interval [a, +∞).
theorem
closure_Iio'
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a : α}
(h : (Set.Iio a).Nonempty)
:
The closure of the interval (-∞, a) is the closed interval (-∞, a], unless a is a bottom
element.
@[simp]
theorem
closure_Iio
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
(a : α)
[NoMinOrder α]
:
The closure of the interval (-∞, a) is the interval (-∞, a].
@[simp]
theorem
closure_Ioo
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a b : α}
(hab : a ≠ b)
:
The closure of the open interval (a, b) is the closed interval [a, b].
@[simp]
theorem
closure_uIoo
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a b : α}
(hab : a ≠ b)
:
@[simp]
theorem
closure_Ioc
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a b : α}
(hab : a ≠ b)
:
The closure of the interval (a, b] is the closed interval [a, b].
@[simp]
theorem
closure_uIoc
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a b : α}
(hab : a ≠ b)
:
@[simp]
theorem
closure_Ico
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a b : α}
(hab : a ≠ b)
:
The closure of the interval [a, b) is the closed interval [a, b].
@[simp]
theorem
interior_Ici'
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a : α}
(ha : (Set.Iio a).Nonempty)
:
theorem
interior_Ici
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMinOrder α]
{a : α}
:
@[simp]
theorem
interior_Iic'
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a : α}
(ha : (Set.Ioi a).Nonempty)
:
theorem
interior_Iic
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMaxOrder α]
{a : α}
:
@[simp]
theorem
interior_Icc
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMinOrder α]
[NoMaxOrder α]
{a b : α}
:
@[simp]
theorem
Icc_mem_nhds_iff
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMinOrder α]
[NoMaxOrder α]
{a b x : α}
:
@[simp]
theorem
interior_Ico
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMinOrder α]
{a b : α}
:
@[simp]
theorem
Ico_mem_nhds_iff
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMinOrder α]
{a b x : α}
:
@[simp]
theorem
interior_Ioc
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMaxOrder α]
{a b : α}
:
@[simp]
theorem
Ioc_mem_nhds_iff
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMaxOrder α]
{a b x : α}
:
theorem
closure_interior_Icc
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a b : α}
(h : a ≠ b)
:
theorem
Ioc_subset_closure_interior
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
(a b : α)
:
theorem
Ico_subset_closure_interior
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
(a b : α)
:
@[simp]
theorem
frontier_Ici'
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a : α}
(ha : (Set.Iio a).Nonempty)
:
theorem
frontier_Ici
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMinOrder α]
{a : α}
:
@[simp]
theorem
frontier_Iic'
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a : α}
(ha : (Set.Ioi a).Nonempty)
:
theorem
frontier_Iic
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMaxOrder α]
{a : α}
:
@[simp]
theorem
frontier_Ioi'
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a : α}
(ha : (Set.Ioi a).Nonempty)
:
theorem
frontier_Ioi
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMaxOrder α]
{a : α}
:
@[simp]
theorem
frontier_Iio'
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a : α}
(ha : (Set.Iio a).Nonempty)
:
theorem
frontier_Iio
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMinOrder α]
{a : α}
:
@[simp]
theorem
frontier_Icc
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMinOrder α]
[NoMaxOrder α]
{a b : α}
(h : a ≤ b)
:
@[simp]
theorem
frontier_Ioo
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a b : α}
(h : a < b)
:
@[simp]
theorem
frontier_Ico
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMinOrder α]
{a b : α}
(h : a < b)
:
@[simp]
theorem
frontier_Ioc
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMaxOrder α]
{a b : α}
(h : a < b)
:
theorem
nhdsWithin_Ioi_neBot'
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a b : α}
(H₁ : (Set.Ioi a).Nonempty)
(H₂ : a ≤ b)
:
(nhdsWithin b (Set.Ioi a)).NeBot
theorem
nhdsWithin_Ioi_neBot
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMaxOrder α]
{a b : α}
(H : a ≤ b)
:
(nhdsWithin b (Set.Ioi a)).NeBot
theorem
nhdsGT_neBot_of_exists_gt
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a : α}
(H : ∃ (b : α), a < b)
:
(nhdsWithin a (Set.Ioi a)).NeBot
instance
nhdsGT_neBot
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMaxOrder α]
(a : α)
:
(nhdsWithin a (Set.Ioi a)).NeBot
theorem
nhdsWithin_Iio_neBot'
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{b c : α}
(H₁ : (Set.Iio c).Nonempty)
(H₂ : b ≤ c)
:
(nhdsWithin b (Set.Iio c)).NeBot
theorem
nhdsWithin_Iio_neBot
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMinOrder α]
{a b : α}
(H : a ≤ b)
:
(nhdsWithin a (Set.Iio b)).NeBot
theorem
nhdsLT_neBot_of_exists_lt
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{b : α}
(H : ∃ (a : α), a < b)
:
(nhdsWithin b (Set.Iio b)).NeBot
@[deprecated nhdsLT_neBot_of_exists_lt (since := "2026-01-16")]
theorem
nhdsWithin_Iio_self_neBot'
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{b : α}
(H : ∃ (a : α), a < b)
:
(nhdsWithin b (Set.Iio b)).NeBot
Alias of nhdsLT_neBot_of_exists_lt.
instance
nhdsLT_neBot
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMinOrder α]
(a : α)
:
(nhdsWithin a (Set.Iio a)).NeBot
theorem
right_nhdsWithin_Ico_neBot
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a b : α}
(H : a < b)
:
(nhdsWithin b (Set.Ico a b)).NeBot
theorem
left_nhdsWithin_Ioc_neBot
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a b : α}
(H : a < b)
:
(nhdsWithin a (Set.Ioc a b)).NeBot
theorem
left_nhdsWithin_Ioo_neBot
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a b : α}
(H : a < b)
:
(nhdsWithin a (Set.Ioo a b)).NeBot
theorem
right_nhdsWithin_Ioo_neBot
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a b : α}
(H : a < b)
:
(nhdsWithin b (Set.Ioo a b)).NeBot
instance
instNeBotNhdsWithinComplSetSingletonOfNontrivial
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
(x : α)
[Nontrivial α]
:
(nhdsWithin x {x}ᶜ).NeBot
theorem
DenselyOrdered.subsingleton_of_discreteTopology
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[DiscreteTopology α]
:
If the order topology for a dense linear ordering is discrete, the space has at most one point.
We would prefer for this to be an instance but even at (priority := 100) this was problematic so
we have deferred this issue. TODO Promote this to an instance!
theorem
Dense.exists_countable_dense_subset_no_bot_top
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[Nontrivial α]
{s : Set α}
[TopologicalSpace.SeparableSpace ↑s]
(hs : Dense s)
:
Let s be a dense set in a nontrivial dense linear order α. If s is a
separable space (e.g., if α has a second countable topology), then there exists a countable
dense subset t ⊆ s such that t does not contain bottom/top elements of α.
theorem
exists_countable_dense_no_bot_top
(α : Type u_1)
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[TopologicalSpace.SeparableSpace α]
[Nontrivial α]
:
If α is a nontrivial separable dense linear order, then there exists a
countable dense set s : Set α that contains neither top nor bottom elements of α.
For a dense set containing both bot and top elements, see
exists_countable_dense_bot_top.
@[simp]
theorem
isClosed_Ico_iff
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a b : α}
:
Set.Ico a b is only closed if it is empty.
@[simp]
theorem
isClosed_Ioc_iff
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a b : α}
:
Set.Ioc a b is only closed if it is empty.
@[simp]
theorem
isClosed_Ioo_iff
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a b : α}
:
Set.Ioo a b is only closed if it is empty.