Neighborhoods to the left and to the right on an OrderTopology

We've seen some properties of left and right neighborhood of a point in an OrderClosedTopology. In an OrderTopology, such neighborhoods can be characterized as the sets containing suitable intervals to the right or to the left of a. We give now these characterizations.

theorem TFAE_mem_nhdsWithin_Ioi {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {b : α} (hab : a < b) (s : Set α) : [s ∈ nhdsWithin a (Set.Ioi a), s ∈ nhdsWithin a (Set.Ioc a b), s ∈ nhdsWithin a (Set.Ioo a b), ∃ u ∈ Set.Ioc a b, Set.Ioo a u ⊆ s, ∃ u ∈ Set.Ioi a, Set.Ioo a u ⊆ s].TFAE

The following statements are equivalent:

0. s is a neighborhood of a within (a, +∞);
1. s is a neighborhood of a within (a, b];
2. s is a neighborhood of a within (a, b);
3. s includes (a, u) for some u ∈ (a, b];
4. s includes (a, u) for some u > a.

theorem mem_nhdsWithin_Ioi_iff_exists_mem_Ioc_Ioo_subset {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {u' : α} {s : Set α} (hu' : a < u') : s ∈ nhdsWithin a (Set.Ioi a) ↔ ∃ u ∈ Set.Ioc a u', Set.Ioo a u ⊆ s

theorem mem_nhdsWithin_Ioi_iff_exists_Ioo_subset' {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {u' : α} {s : Set α} (hu' : a < u') : s ∈ nhdsWithin a (Set.Ioi a) ↔ ∃ u ∈ Set.Ioi a, Set.Ioo a u ⊆ s

A set is a neighborhood of a within (a, +∞) if and only if it contains an interval (a, u) with a < u < u', provided a is not a top element.

theorem nhdsWithin_Ioi_basis' {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (h : ∃ (b : α), a < b) : (nhdsWithin a (Set.Ioi a)).HasBasis (fun (x : α) => a < x) (Set.Ioo a)

theorem nhdsWithin_Ioi_basis {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] (a : α) : (nhdsWithin a (Set.Ioi a)).HasBasis (fun (x : α) => a < x) (Set.Ioo a)

theorem nhdsWithin_Ioi_eq_bot_iff {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} : nhdsWithin a (Set.Ioi a) = ⊥ ↔ IsTop a ∨ ∃ (b : α), a ⋖ b

theorem mem_nhdsWithin_Ioi_iff_exists_Ioo_subset {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] {a : α} {s : Set α} : s ∈ nhdsWithin a (Set.Ioi a) ↔ ∃ u ∈ Set.Ioi a, Set.Ioo a u ⊆ s

A set is a neighborhood of a within (a, +∞) if and only if it contains an interval (a, u) with a < u.

theorem countable_setOf_isolated_right {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] : {x : α | nhdsWithin x (Set.Ioi x) = ⊥}.Countable

The set of points which are isolated on the right is countable when the space is second-countable.

theorem countable_setOf_isolated_left {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] : {x : α | nhdsWithin x (Set.Iio x) = ⊥}.Countable

The set of points which are isolated on the left is countable when the space is second-countable.

theorem mem_nhdsWithin_Ioi_iff_exists_Ioc_subset {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] [DenselyOrdered α] {a : α} {s : Set α} : s ∈ nhdsWithin a (Set.Ioi a) ↔ ∃ u ∈ Set.Ioi a, Set.Ioc a u ⊆ s

A set is a neighborhood of a within (a, +∞) if and only if it contains an interval (a, u] with a < u.

theorem TFAE_mem_nhdsWithin_Iio {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {b : α} (h : a < b) (s : Set α) : [s ∈ nhdsWithin b (Set.Iio b), s ∈ nhdsWithin b (Set.Ico a b), s ∈ nhdsWithin b (Set.Ioo a b), ∃ l ∈ Set.Ico a b, Set.Ioo l b ⊆ s, ∃ l ∈ Set.Iio b, Set.Ioo l b ⊆ s].TFAE

The following statements are equivalent:

0. s is a neighborhood of b within (-∞, b)
1. s is a neighborhood of b within [a, b)
2. s is a neighborhood of b within (a, b)
3. s includes (l, b) for some l ∈ [a, b)
4. s includes (l, b) for some l < b

theorem mem_nhdsWithin_Iio_iff_exists_mem_Ico_Ioo_subset {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {l' : α} {s : Set α} (hl' : l' < a) : s ∈ nhdsWithin a (Set.Iio a) ↔ ∃ l ∈ Set.Ico l' a, Set.Ioo l a ⊆ s

theorem mem_nhdsWithin_Iio_iff_exists_Ioo_subset' {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {l' : α} {s : Set α} (hl' : l' < a) : s ∈ nhdsWithin a (Set.Iio a) ↔ ∃ l ∈ Set.Iio a, Set.Ioo l a ⊆ s

A set is a neighborhood of a within (-∞, a) if and only if it contains an interval (l, a) with l < a, provided a is not a bottom element.

theorem mem_nhdsWithin_Iio_iff_exists_Ioo_subset {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] {a : α} {s : Set α} : s ∈ nhdsWithin a (Set.Iio a) ↔ ∃ l ∈ Set.Iio a, Set.Ioo l a ⊆ s

A set is a neighborhood of a within (-∞, a) if and only if it contains an interval (l, a) with l < a.

theorem mem_nhdsWithin_Iio_iff_exists_Ico_subset {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] [DenselyOrdered α] {a : α} {s : Set α} : s ∈ nhdsWithin a (Set.Iio a) ↔ ∃ l ∈ Set.Iio a, Set.Ico l a ⊆ s

A set is a neighborhood of a within (-∞, a) if and only if it contains an interval [l, a) with l < a.

theorem nhdsWithin_Iio_basis' {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (h : ∃ (b : α), b < a) : (nhdsWithin a (Set.Iio a)).HasBasis (fun (x : α) => x < a) fun (x : α) => Set.Ioo x a

theorem nhdsWithin_Iio_basis {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] (a : α) : (nhdsWithin a (Set.Iio a)).HasBasis (fun (x : α) => x < a) fun (x : α) => Set.Ioo x a

theorem nhdsWithin_Iio_eq_bot_iff {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} : nhdsWithin a (Set.Iio a) = ⊥ ↔ IsBot a ∨ ∃ (b : α), b ⋖ a

theorem TFAE_mem_nhdsWithin_Ici {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {b : α} (hab : a < b) (s : Set α) : [s ∈ nhdsWithin a (Set.Ici a), s ∈ nhdsWithin a (Set.Icc a b), s ∈ nhdsWithin a (Set.Ico a b), ∃ u ∈ Set.Ioc a b, Set.Ico a u ⊆ s, ∃ u ∈ Set.Ioi a, Set.Ico a u ⊆ s].TFAE

The following statements are equivalent:

0. s is a neighborhood of a within [a, +∞);
1. s is a neighborhood of a within [a, b];
2. s is a neighborhood of a within [a, b);
3. s includes [a, u) for some u ∈ (a, b];
4. s includes [a, u) for some u > a.

theorem mem_nhdsWithin_Ici_iff_exists_mem_Ioc_Ico_subset {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {u' : α} {s : Set α} (hu' : a < u') : s ∈ nhdsWithin a (Set.Ici a) ↔ ∃ u ∈ Set.Ioc a u', Set.Ico a u ⊆ s

theorem mem_nhdsWithin_Ici_iff_exists_Ico_subset' {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {u' : α} {s : Set α} (hu' : a < u') : s ∈ nhdsWithin a (Set.Ici a) ↔ ∃ u ∈ Set.Ioi a, Set.Ico a u ⊆ s

A set is a neighborhood of a within [a, +∞) if and only if it contains an interval [a, u) with a < u < u', provided a is not a top element.

theorem mem_nhdsWithin_Ici_iff_exists_Ico_subset {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] {a : α} {s : Set α} : s ∈ nhdsWithin a (Set.Ici a) ↔ ∃ u ∈ Set.Ioi a, Set.Ico a u ⊆ s

A set is a neighborhood of a within [a, +∞) if and only if it contains an interval [a, u) with a < u.

theorem nhdsWithin_Ici_basis_Ico {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] (a : α) : (nhdsWithin a (Set.Ici a)).HasBasis (fun (u : α) => a < u) (Set.Ico a)

theorem nhdsWithin_Ici_basis_Icc {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] [DenselyOrdered α] {a : α} : (nhdsWithin a (Set.Ici a)).HasBasis (fun (x : α) => a < x) (Set.Icc a)

The filter of right neighborhoods has a basis of closed intervals.

theorem mem_nhdsWithin_Ici_iff_exists_Icc_subset {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] [DenselyOrdered α] {a : α} {s : Set α} : s ∈ nhdsWithin a (Set.Ici a) ↔ ∃ (u : α), a < u ∧ Set.Icc a u ⊆ s

A set is a neighborhood of a within [a, +∞) if and only if it contains an interval [a, u] with a < u.

theorem TFAE_mem_nhdsWithin_Iic {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {b : α} (h : a < b) (s : Set α) : [s ∈ nhdsWithin b (Set.Iic b), s ∈ nhdsWithin b (Set.Icc a b), s ∈ nhdsWithin b (Set.Ioc a b), ∃ l ∈ Set.Ico a b, Set.Ioc l b ⊆ s, ∃ l ∈ Set.Iio b, Set.Ioc l b ⊆ s].TFAE

The following statements are equivalent:

0. s is a neighborhood of b within (-∞, b]
1. s is a neighborhood of b within [a, b]
2. s is a neighborhood of b within (a, b]
3. s includes (l, b] for some l ∈ [a, b)
4. s includes (l, b] for some l < b

theorem mem_nhdsWithin_Iic_iff_exists_mem_Ico_Ioc_subset {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {l' : α} {s : Set α} (hl' : l' < a) : s ∈ nhdsWithin a (Set.Iic a) ↔ ∃ l ∈ Set.Ico l' a, Set.Ioc l a ⊆ s

theorem mem_nhdsWithin_Iic_iff_exists_Ioc_subset' {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {l' : α} {s : Set α} (hl' : l' < a) : s ∈ nhdsWithin a (Set.Iic a) ↔ ∃ l ∈ Set.Iio a, Set.Ioc l a ⊆ s

A set is a neighborhood of a within (-∞, a] if and only if it contains an interval (l, a] with l < a, provided a is not a bottom element.

theorem mem_nhdsWithin_Iic_iff_exists_Ioc_subset {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] {a : α} {s : Set α} : s ∈ nhdsWithin a (Set.Iic a) ↔ ∃ l ∈ Set.Iio a, Set.Ioc l a ⊆ s

A set is a neighborhood of a within (-∞, a] if and only if it contains an interval (l, a] with l < a.

theorem mem_nhdsWithin_Iic_iff_exists_Icc_subset {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] [DenselyOrdered α] {a : α} {s : Set α} : s ∈ nhdsWithin a (Set.Iic a) ↔ ∃ l < a, Set.Icc l a ⊆ s

A set is a neighborhood of a within (-∞, a] if and only if it contains an interval [l, a] with l < a.

theorem nhdsWithin_Iic_basis_Icc {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] [DenselyOrdered α] {a : α} : (nhdsWithin a (Set.Iic a)).HasBasis (fun (x : α) => x < a) fun (x : α) => Set.Icc x a

The filter of left neighborhoods has a basis of closed intervals.

theorem nhds_eq_iInf_abs_sub {α : Type u_1} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] (a : α) : nhds a = ⨅ (r : α), ⨅ (_ : r > 0), Filter.principal {b : α | |a - b| < r}

theorem orderTopology_of_nhds_abs {α : Type u_4} [TopologicalSpace α] [LinearOrderedAddCommGroup α] (h_nhds : ∀ (a : α), nhds a = ⨅ (r : α), ⨅ (_ : r > 0), Filter.principal {b : α | |a - b| < r}) : OrderTopology α

theorem LinearOrderedAddCommGroup.tendsto_nhds {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] {f : β → α} {x : Filter β} {a : α} : Filter.Tendsto f x (nhds a) ↔ ∀ ε > 0, ∀ᶠ (b : β) in x, |f b - a| < ε

theorem eventually_abs_sub_lt {α : Type u_1} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] (a : α) {ε : α} (hε : 0 < ε) : ∀ᶠ (x : α) in nhds a, |x - a| < ε

theorem Filter.Tendsto.add_atTop {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] {l : Filter β} {f : β → α} {g : β → α} {C : α} (hf : Filter.Tendsto f l (nhds C)) (hg : Filter.Tendsto g l Filter.atTop) : Filter.Tendsto (fun (x : β) => f x + g x) l Filter.atTop

In a linearly ordered additive commutative group with the order topology, if f tends to C and g tends to atTop then f + g tends to atTop.

theorem Filter.Tendsto.add_atBot {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] {l : Filter β} {f : β → α} {g : β → α} {C : α} (hf : Filter.Tendsto f l (nhds C)) (hg : Filter.Tendsto g l Filter.atBot) : Filter.Tendsto (fun (x : β) => f x + g x) l Filter.atBot

In a linearly ordered additive commutative group with the order topology, if f tends to C and g tends to atBot then f + g tends to atBot.

theorem Filter.Tendsto.atTop_add {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] {l : Filter β} {f : β → α} {g : β → α} {C : α} (hf : Filter.Tendsto f l Filter.atTop) (hg : Filter.Tendsto g l (nhds C)) : Filter.Tendsto (fun (x : β) => f x + g x) l Filter.atTop

In a linearly ordered additive commutative group with the order topology, if f tends to atTop and g tends to C then f + g tends to atTop.

theorem Filter.Tendsto.atBot_add {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] {l : Filter β} {f : β → α} {g : β → α} {C : α} (hf : Filter.Tendsto f l Filter.atBot) (hg : Filter.Tendsto g l (nhds C)) : Filter.Tendsto (fun (x : β) => f x + g x) l Filter.atBot

In a linearly ordered additive commutative group with the order topology, if f tends to atBot and g tends to C then f + g tends to atBot.

theorem nhds_basis_abs_sub_lt {α : Type u_1} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] [NoMaxOrder α] (a : α) : (nhds a).HasBasis (fun (ε : α) => 0 < ε) fun (ε : α) => {b : α | |b - a| < ε}

theorem nhds_basis_Ioo_pos {α : Type u_1} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] [NoMaxOrder α] (a : α) : (nhds a).HasBasis (fun (ε : α) => 0 < ε) fun (ε : α) => Set.Ioo (a - ε) (a + ε)

theorem nhds_basis_Icc_pos {α : Type u_1} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] [NoMaxOrder α] [DenselyOrdered α] (a : α) : (nhds a).HasBasis (fun (x : α) => 0 < x) fun (ε : α) => Set.Icc (a - ε) (a + ε)

theorem nhds_basis_zero_abs_sub_lt (α : Type u_1) [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] [NoMaxOrder α] : (nhds 0).HasBasis (fun (ε : α) => 0 < ε) fun (ε : α) => {b : α | |b| < ε}

theorem nhds_basis_Ioo_pos_of_pos {α : Type u_1} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] [NoMaxOrder α] {a : α} (ha : 0 < a) : (nhds a).HasBasis (fun (ε : α) => 0 < ε ∧ ε ≤ a) fun (ε : α) => Set.Ioo (a - ε) (a + ε)

If a is positive we can form a basis from only nonnegative Set.Ioo intervals

theorem Set.OrdConnected.mem_nhdsWithin_Ici {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] {S : Set α} (hS : S.OrdConnected) {x : α} {y : α} (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) : S ∈ nhdsWithin x (Set.Ici x)

If S is order-connected and contains two points x < y, then S is a right neighbourhood of x.

theorem Set.OrdConnected.mem_nhdsWithin_Ioi {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] {S : Set α} (hS : S.OrdConnected) {x : α} {y : α} (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) : S ∈ nhdsWithin x (Set.Ioi x)

If S is order-connected and contains two points x < y, then S is a punctured right neighbourhood of x.

theorem Set.OrdConnected.mem_nhdsWithin_Iic {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] {S : Set α} (hS : S.OrdConnected) {x : α} {y : α} (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) : S ∈ nhdsWithin y (Set.Iic y)

If S is order-connected and contains two points x < y, then S is a left neighbourhood of y.

theorem Set.OrdConnected.mem_nhdsWithin_Iio {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] {S : Set α} (hS : S.OrdConnected) {x : α} {y : α} (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) : S ∈ nhdsWithin y (Set.Iio y)

If S is order-connected and contains two points x < y, then S is a punctured left neighbourhood of y.