Order topology on a densely ordered set

theorem closure_Ioi' {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (h : (Set.Ioi a).Nonempty) : closure (Set.Ioi a) = Set.Ici a

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 α] : closure (Set.Ioi a) = Set.Ici a

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) : closure (Set.Iio a) = Set.Iic a

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 α] : closure (Set.Iio a) = Set.Iic a

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) : closure (Set.Ioo a b) = Set.Icc 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) : closure (Set.Ioc a b) = Set.Icc 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) : closure (Set.Ico a b) = Set.Icc 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) : interior (Set.Ici a) = Set.Ioi a

theorem interior_Ici {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] {a : α} : interior (Set.Ici a) = Set.Ioi a

@[simp]

theorem interior_Iic' {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (ha : (Set.Ioi a).Nonempty) : interior (Set.Iic a) = Set.Iio a

theorem interior_Iic {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] {a : α} : interior (Set.Iic a) = Set.Iio a

@[simp]

theorem interior_Icc {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] {a b : α} : interior (Set.Icc a b) = Set.Ioo a b

@[simp]

theorem Icc_mem_nhds_iff {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] {a b x : α} : Set.Icc a b ∈ nhds x ↔ x ∈ Set.Ioo a b

@[simp]

theorem interior_Ico {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] {a b : α} : interior (Set.Ico a b) = Set.Ioo a b

@[simp]

theorem Ico_mem_nhds_iff {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] {a b x : α} : Set.Ico a b ∈ nhds x ↔ x ∈ Set.Ioo a b

@[simp]

theorem interior_Ioc {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] {a b : α} : interior (Set.Ioc a b) = Set.Ioo a b

@[simp]

theorem Ioc_mem_nhds_iff {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] {a b x : α} : Set.Ioc a b ∈ nhds x ↔ x ∈ Set.Ioo a b

theorem closure_interior_Icc {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α} (h : a ≠ b) : closure (interior (Set.Icc a b)) = Set.Icc a b

theorem Ioc_subset_closure_interior {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] (a b : α) : Set.Ioc a b ⊆ closure (interior (Set.Ioc a b))

theorem Ico_subset_closure_interior {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] (a b : α) : Set.Ico a b ⊆ closure (interior (Set.Ico a b))

@[simp]

theorem frontier_Ici' {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (ha : (Set.Iio a).Nonempty) : frontier (Set.Ici a) = {a}

theorem frontier_Ici {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] {a : α} : frontier (Set.Ici a) = {a}

@[simp]

theorem frontier_Iic' {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (ha : (Set.Ioi a).Nonempty) : frontier (Set.Iic a) = {a}

theorem frontier_Iic {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] {a : α} : frontier (Set.Iic a) = {a}

@[simp]

theorem frontier_Ioi' {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (ha : (Set.Ioi a).Nonempty) : frontier (Set.Ioi a) = {a}

theorem frontier_Ioi {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] {a : α} : frontier (Set.Ioi a) = {a}

@[simp]

theorem frontier_Iio' {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (ha : (Set.Iio a).Nonempty) : frontier (Set.Iio a) = {a}

theorem frontier_Iio {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] {a : α} : frontier (Set.Iio a) = {a}

@[simp]

theorem frontier_Icc {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] {a b : α} (h : a ≤ b) : frontier (Set.Icc a b) = {a, b}

@[simp]

theorem frontier_Ioo {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α} (h : a < b) : frontier (Set.Ioo a b) = {a, b}

@[simp]

theorem frontier_Ico {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] {a b : α} (h : a < b) : frontier (Set.Ico a b) = {a, b}

@[simp]

theorem frontier_Ioc {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] {a b : α} (h : a < b) : frontier (Set.Ioc a b) = {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 nhdsWithin_Ioi_self_neBot' {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (H : (Set.Ioi a).Nonempty) : (nhdsWithin a (Set.Ioi a)).NeBot

instance nhdsWithin_Ioi_self_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 nhdsWithin_Iio_self_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_nhdsWithin_Iio_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) : Filter.comap Subtype.val (nhdsWithin b (Set.Iio b)) = Filter.atTop

theorem comap_coe_nhdsWithin_Ioi_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) : Filter.comap Subtype.val (nhdsWithin a (Set.Ioi a)) = Filter.atBot

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) : Filter.map Subtype.val Filter.atTop = nhdsWithin b (Set.Iio b)

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) : Filter.map Subtype.val Filter.atBot = nhdsWithin a (Set.Ioi a)

theorem comap_coe_Ioo_nhdsWithin_Iio {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] (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} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] (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} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] (a : α) : Filter.comap Subtype.val (nhdsWithin a (Set.Ioi a)) = Filter.atBot

theorem comap_coe_Iio_nhdsWithin_Iio {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] (a : α) : Filter.comap Subtype.val (nhdsWithin a (Set.Iio a)) = Filter.atTop

@[simp]

theorem map_coe_Ioo_atTop {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {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} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {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} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] (a : α) : Filter.map Subtype.val Filter.atBot = nhdsWithin a (Set.Ioi a)

@[simp]

theorem map_coe_Iio_atTop {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] (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} [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) : ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∉ t) ∧ ∀ (x : α), IsTop x → x ∉ t

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 α] : ∃ (s : Set α), s.Countable ∧ Dense s ∧ (∀ (x : α), IsBot x → x ∉ s) ∧ ∀ (x : α), IsTop x → x ∉ s

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.