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_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_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
nhdsWithin_Iio_self_neBot'
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{b : α}
(H : (Set.Iio b).Nonempty)
:
(nhdsWithin b (Set.Iio b)).NeBot
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
theorem
comap_coe_nhdsLT_of_Ioo_subset
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{b : α}
{s : Set α}
(hb : s ⊆ Set.Iio b)
(hs : s.Nonempty → ∃ a < b, Set.Ioo a b ⊆ s)
:
theorem
comap_coe_nhdsGT_of_Ioo_subset
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a : α}
{s : Set α}
(ha : s ⊆ Set.Ioi a)
(hs : s.Nonempty → ∃ b > a, Set.Ioo a b ⊆ s)
:
theorem
map_coe_atTop_of_Ioo_subset
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{b : α}
{s : Set α}
(hb : s ⊆ Set.Iio b)
(hs : ∀ a' < b, ∃ a < b, Set.Ioo a b ⊆ s)
:
theorem
map_coe_atBot_of_Ioo_subset
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a : α}
{s : Set α}
(ha : s ⊆ Set.Ioi a)
(hs : ∀ b' > a, ∃ b > a, Set.Ioo a b ⊆ s)
:
theorem
comap_coe_Ioo_nhdsLT
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
(a b : α)
:
The atTop filter for an open interval Ioo a b comes from the left-neighbourhoods filter at
the right endpoint in the ambient order.
theorem
comap_coe_Ioo_nhdsGT
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
(a b : α)
:
The atBot filter for an open interval Ioo a b comes from the right-neighbourhoods filter at
the left endpoint in the ambient order.
theorem
comap_coe_Ioi_nhdsGT
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
(a : α)
:
theorem
comap_coe_Iio_nhdsLT
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
(a : α)
:
@[simp]
theorem
map_coe_Ioo_atTop
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a b : α}
(h : a < b)
:
@[simp]
theorem
map_coe_Ioo_atBot
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a b : α}
(h : a < b)
:
@[simp]
theorem
map_coe_Ioi_atBot
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
(a : α)
:
@[simp]
theorem
map_coe_Iio_atTop
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
(a : α)
:
@[simp]
theorem
tendsto_comp_coe_Ioo_atTop
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a b : α}
{l : Filter β}
{f : α → β}
(h : a < b)
:
Filter.Tendsto (fun (x : ↑(Set.Ioo a b)) => f ↑x) Filter.atTop l ↔ Filter.Tendsto f (nhdsWithin b (Set.Iio b)) l
@[simp]
theorem
tendsto_comp_coe_Ioo_atBot
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a b : α}
{l : Filter β}
{f : α → β}
(h : a < b)
:
Filter.Tendsto (fun (x : ↑(Set.Ioo a b)) => f ↑x) Filter.atBot l ↔ Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) l
@[simp]
theorem
tendsto_comp_coe_Ioi_atBot
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a : α}
{l : Filter β}
{f : α → β}
:
Filter.Tendsto (fun (x : ↑(Set.Ioi a)) => f ↑x) Filter.atBot l ↔ Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) l
@[simp]
theorem
tendsto_comp_coe_Iio_atTop
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a : α}
{l : Filter β}
{f : α → β}
:
Filter.Tendsto (fun (x : ↑(Set.Iio a)) => f ↑x) Filter.atTop l ↔ Filter.Tendsto f (nhdsWithin a (Set.Iio a)) l
@[simp]
theorem
tendsto_Ioo_atTop
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a b : α}
{l : Filter β}
{f : β → ↑(Set.Ioo a b)}
:
Filter.Tendsto f l Filter.atTop ↔ Filter.Tendsto (fun (x : β) => ↑(f x)) l (nhdsWithin b (Set.Iio b))
@[simp]
theorem
tendsto_Ioo_atBot
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a b : α}
{l : Filter β}
{f : β → ↑(Set.Ioo a b)}
:
Filter.Tendsto f l Filter.atBot ↔ Filter.Tendsto (fun (x : β) => ↑(f x)) l (nhdsWithin a (Set.Ioi a))
@[simp]
theorem
tendsto_Ioi_atBot
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a : α}
{l : Filter β}
{f : β → ↑(Set.Ioi a)}
:
Filter.Tendsto f l Filter.atBot ↔ Filter.Tendsto (fun (x : β) => ↑(f x)) l (nhdsWithin a (Set.Ioi a))
@[simp]
theorem
tendsto_Iio_atTop
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
{a : α}
{l : Filter β}
{f : β → ↑(Set.Iio a)}
:
Filter.Tendsto f l Filter.atTop ↔ Filter.Tendsto (fun (x : β) => ↑(f x)) l (nhdsWithin a (Set.Iio a))
instance
instNeBotNhdsWithinComplSetSingletonOfNontrivial
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
(x : α)
[Nontrivial α]
:
(nhdsWithin x {x}ᶜ).NeBot
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.