# Order topology on a densely ordered set #

theorem closure_Ioi' {α : Type u_1} [] [] [] [] {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} [] [] [] [] (a : α) [] :

The closure of the interval (a, +∞) is the closed interval [a, +∞).

theorem closure_Iio' {α : Type u_1} [] [] [] [] {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} [] [] [] [] (a : α) [] :

The closure of the interval (-∞, a) is the interval (-∞, a].

@[simp]
theorem closure_Ioo {α : Type u_1} [] [] [] [] {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} [] [] [] [] {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} [] [] [] [] {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} [] [] [] [] {a : α} (ha : (Set.Iio a).Nonempty) :
theorem interior_Ici {α : Type u_1} [] [] [] [] [] {a : α} :
@[simp]
theorem interior_Iic' {α : Type u_1} [] [] [] [] {a : α} (ha : (Set.Ioi a).Nonempty) :
theorem interior_Iic {α : Type u_1} [] [] [] [] [] {a : α} :
@[simp]
theorem interior_Icc {α : Type u_1} [] [] [] [] [] [] {a : α} {b : α} :
@[simp]
theorem Icc_mem_nhds_iff {α : Type u_1} [] [] [] [] [] [] {a : α} {b : α} {x : α} :
@[simp]
theorem interior_Ico {α : Type u_1} [] [] [] [] [] {a : α} {b : α} :
@[simp]
theorem Ico_mem_nhds_iff {α : Type u_1} [] [] [] [] [] {a : α} {b : α} {x : α} :
@[simp]
theorem interior_Ioc {α : Type u_1} [] [] [] [] [] {a : α} {b : α} :
@[simp]
theorem Ioc_mem_nhds_iff {α : Type u_1} [] [] [] [] [] {a : α} {b : α} {x : α} :
theorem closure_interior_Icc {α : Type u_1} [] [] [] [] {a : α} {b : α} (h : a b) :
theorem Ioc_subset_closure_interior {α : Type u_1} [] [] [] [] (a : α) (b : α) :
theorem Ico_subset_closure_interior {α : Type u_1} [] [] [] [] (a : α) (b : α) :
@[simp]
theorem frontier_Ici' {α : Type u_1} [] [] [] [] {a : α} (ha : (Set.Iio a).Nonempty) :
theorem frontier_Ici {α : Type u_1} [] [] [] [] [] {a : α} :
@[simp]
theorem frontier_Iic' {α : Type u_1} [] [] [] [] {a : α} (ha : (Set.Ioi a).Nonempty) :
theorem frontier_Iic {α : Type u_1} [] [] [] [] [] {a : α} :
@[simp]
theorem frontier_Ioi' {α : Type u_1} [] [] [] [] {a : α} (ha : (Set.Ioi a).Nonempty) :
theorem frontier_Ioi {α : Type u_1} [] [] [] [] [] {a : α} :
@[simp]
theorem frontier_Iio' {α : Type u_1} [] [] [] [] {a : α} (ha : (Set.Iio a).Nonempty) :
theorem frontier_Iio {α : Type u_1} [] [] [] [] [] {a : α} :
@[simp]
theorem frontier_Icc {α : Type u_1} [] [] [] [] [] [] {a : α} {b : α} (h : a b) :
frontier (Set.Icc a b) = {a, b}
@[simp]
theorem frontier_Ioo {α : Type u_1} [] [] [] [] {a : α} {b : α} (h : a < b) :
frontier (Set.Ioo a b) = {a, b}
@[simp]
theorem frontier_Ico {α : Type u_1} [] [] [] [] [] {a : α} {b : α} (h : a < b) :
frontier (Set.Ico a b) = {a, b}
@[simp]
theorem frontier_Ioc {α : Type u_1} [] [] [] [] [] {a : α} {b : α} (h : a < b) :
frontier (Set.Ioc a b) = {a, b}
theorem nhdsWithin_Ioi_neBot' {α : Type u_1} [] [] [] [] {a : α} {b : α} (H₁ : (Set.Ioi a).Nonempty) (H₂ : a b) :
(nhdsWithin b (Set.Ioi a)).NeBot
theorem nhdsWithin_Ioi_neBot {α : Type u_1} [] [] [] [] [] {a : α} {b : α} (H : a b) :
(nhdsWithin b (Set.Ioi a)).NeBot
theorem nhdsWithin_Ioi_self_neBot' {α : Type u_1} [] [] [] [] {a : α} (H : (Set.Ioi a).Nonempty) :
(nhdsWithin a (Set.Ioi a)).NeBot
instance nhdsWithin_Ioi_self_neBot {α : Type u_1} [] [] [] [] [] (a : α) :
(nhdsWithin a (Set.Ioi a)).NeBot
Equations
• =
theorem nhdsWithin_Iio_neBot' {α : Type u_1} [] [] [] [] {b : α} {c : α} (H₁ : (Set.Iio c).Nonempty) (H₂ : b c) :
(nhdsWithin b (Set.Iio c)).NeBot
theorem nhdsWithin_Iio_neBot {α : Type u_1} [] [] [] [] [] {a : α} {b : α} (H : a b) :
(nhdsWithin a (Set.Iio b)).NeBot
theorem nhdsWithin_Iio_self_neBot' {α : Type u_1} [] [] [] [] {b : α} (H : (Set.Iio b).Nonempty) :
(nhdsWithin b (Set.Iio b)).NeBot
instance nhdsWithin_Iio_self_neBot {α : Type u_1} [] [] [] [] [] (a : α) :
(nhdsWithin a (Set.Iio a)).NeBot
Equations
• =
theorem right_nhdsWithin_Ico_neBot {α : Type u_1} [] [] [] [] {a : α} {b : α} (H : a < b) :
(nhdsWithin b (Set.Ico a b)).NeBot
theorem left_nhdsWithin_Ioc_neBot {α : Type u_1} [] [] [] [] {a : α} {b : α} (H : a < b) :
(nhdsWithin a (Set.Ioc a b)).NeBot
theorem left_nhdsWithin_Ioo_neBot {α : Type u_1} [] [] [] [] {a : α} {b : α} (H : a < b) :
(nhdsWithin a (Set.Ioo a b)).NeBot
theorem right_nhdsWithin_Ioo_neBot {α : Type u_1} [] [] [] [] {a : α} {b : α} (H : a < b) :
(nhdsWithin b (Set.Ioo a b)).NeBot
theorem comap_coe_nhdsWithin_Iio_of_Ioo_subset {α : Type u_1} [] [] [] [] {b : α} {s : Set α} (hb : s ) (hs : s.Nonemptya < b, Set.Ioo a b s) :
Filter.comap Subtype.val (nhdsWithin b (Set.Iio b)) = Filter.atTop
theorem comap_coe_nhdsWithin_Ioi_of_Ioo_subset {α : Type u_1} [] [] [] [] {a : α} {s : Set α} (ha : s ) (hs : s.Nonemptyb > a, Set.Ioo a b s) :
Filter.comap Subtype.val (nhdsWithin a (Set.Ioi a)) = Filter.atBot
theorem map_coe_atTop_of_Ioo_subset {α : Type u_1} [] [] [] [] {b : α} {s : Set α} (hb : s ) (hs : a' < b, a < b, Set.Ioo a b s) :
Filter.map Subtype.val Filter.atTop = nhdsWithin b (Set.Iio b)
theorem map_coe_atBot_of_Ioo_subset {α : Type u_1} [] [] [] [] {a : α} {s : Set α} (ha : s ) (hs : b' > a, b > a, Set.Ioo a b s) :
Filter.map Subtype.val Filter.atBot = nhdsWithin a (Set.Ioi a)
theorem comap_coe_Ioo_nhdsWithin_Iio {α : Type u_1} [] [] [] [] (a : α) (b : α) :
Filter.comap Subtype.val (nhdsWithin b (Set.Iio b)) = Filter.atTop

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_nhdsWithin_Ioi {α : Type u_1} [] [] [] [] (a : α) (b : α) :
Filter.comap Subtype.val (nhdsWithin a (Set.Ioi a)) = Filter.atBot

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_nhdsWithin_Ioi {α : Type u_1} [] [] [] [] (a : α) :
Filter.comap Subtype.val (nhdsWithin a (Set.Ioi a)) = Filter.atBot
theorem comap_coe_Iio_nhdsWithin_Iio {α : Type u_1} [] [] [] [] (a : α) :
Filter.comap Subtype.val (nhdsWithin a (Set.Iio a)) = Filter.atTop
@[simp]
theorem map_coe_Ioo_atTop {α : Type u_1} [] [] [] [] {a : α} {b : α} (h : a < b) :
Filter.map Subtype.val Filter.atTop = nhdsWithin b (Set.Iio b)
@[simp]
theorem map_coe_Ioo_atBot {α : Type u_1} [] [] [] [] {a : α} {b : α} (h : a < b) :
Filter.map Subtype.val Filter.atBot = nhdsWithin a (Set.Ioi a)
@[simp]
theorem map_coe_Ioi_atBot {α : Type u_1} [] [] [] [] (a : α) :
Filter.map Subtype.val Filter.atBot = nhdsWithin a (Set.Ioi a)
@[simp]
theorem map_coe_Iio_atTop {α : Type u_1} [] [] [] [] (a : α) :
Filter.map Subtype.val Filter.atTop = nhdsWithin a (Set.Iio a)
@[simp]
theorem tendsto_comp_coe_Ioo_atTop {α : Type u_1} {β : Type u_2} [] [] [] [] {a : α} {b : α} {l : } {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} [] [] [] [] {a : α} {b : α} {l : } {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} [] [] [] [] {a : α} {l : } {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} [] [] [] [] {a : α} {l : } {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} [] [] [] [] {a : α} {b : α} {l : } {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} [] [] [] [] {a : α} {b : α} {l : } {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} [] [] [] [] {a : α} {l : } {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} [] [] [] [] {a : α} {l : } {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} [] [] [] [] (x : α) [] :
(nhdsWithin x {x}).NeBot
Equations
• =
theorem Dense.exists_countable_dense_subset_no_bot_top {α : Type u_1} [] [] [] [] [] {s : Set α} (hs : ) :
ts, t.Countable (∀ (x : α), xt) ∀ (x : α), xt

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) [] [] [] [] [] :
∃ (s : Set α), s.Countable (∀ (x : α), xs) ∀ (x : α), xs

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.