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_nhdsGT {α : 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_nhdsGT_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_nhdsGT_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 nhdsGT_basis_of_exists_gt {α : 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 nhdsGT_basis {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] (a : α) : (nhdsWithin a (Set.Ioi a)).HasBasis (fun (x : α) => a < x) (Set.Ioo a)

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

theorem mem_nhdsGT_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 countable_setOf_isolated_right_within {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {s : Set α} : {x : α | x ∈ s ∧ nhdsWithin x (s ∩ Set.Ioi x) = ⊥}.Countable

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

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

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

theorem mem_nhdsGT_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_nhdsLT {α : 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_nhdsLT_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_nhdsLT_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_nhdsLT_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_nhdsLT_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 nhdsLT_basis_of_exists_lt {α : 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 nhdsLT_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 nhdsLT_eq_bot_iff {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} : nhdsWithin a (Set.Iio a) = ⊥ ↔ IsBot a ∨ ∃ (b : α), b ⋖ a

theorem TFAE_mem_nhdsGE {α : 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_nhdsGE_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_nhdsGE_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_nhdsGE_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 nhdsGE_basis_Ico {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] (a : α) : (nhdsWithin a (Set.Ici a)).HasBasis (fun (u : α) => a < u) (Set.Ico a)

theorem nhdsGE_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_nhdsGE_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_nhdsLE {α : 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_nhdsLE_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_nhdsLE_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_nhdsLE_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_nhdsLE_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 nhdsLE_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_mabs_div {α : Type u_1} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] (a : α) : nhds a = ⨅ (r : α), ⨅ (_ : r > 1), Filter.principal {b : α | mabs (a / b) < r}

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

theorem orderTopology_of_nhds_mabs {α : Type u_4} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] (h_nhds : ∀ (a : α), nhds a = ⨅ (r : α), ⨅ (_ : r > 1), Filter.principal {b : α | mabs (a / b) < r}) : OrderTopology α

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

theorem LinearOrderedCommGroup.tendsto_nhds {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] {f : β → α} {x : Filter β} {a : α} : Filter.Tendsto f x (nhds a) ↔ ∀ ε > 1, ∀ᶠ (b : β) in x, mabs (f b / a) < ε

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

theorem eventually_mabs_div_lt {α : Type u_1} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] (a : α) {ε : α} (hε : 1 < ε) : ∀ᶠ (x : α) in nhds a, mabs (x / a) < ε

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

theorem Filter.Tendsto.mul_atTop' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] {l : Filter β} {f g : β → α} {C : α} (hf : Tendsto f l (nhds C)) (hg : Tendsto g l atTop) : Tendsto (fun (x : β) => f x * g x) l atTop

In a linearly ordered 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_atTop {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [OrderTopology α] {l : Filter β} {f g : β → α} {C : α} (hf : Tendsto f l (nhds C)) (hg : Tendsto g l atTop) : Tendsto (fun (x : β) => f x + g x) l 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.mul_atBot' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] {l : Filter β} {f g : β → α} {C : α} (hf : Tendsto f l (nhds C)) (hg : Tendsto g l atBot) : Tendsto (fun (x : β) => f x * g x) l atBot

In a linearly ordered 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.add_atBot {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [OrderTopology α] {l : Filter β} {f g : β → α} {C : α} (hf : Tendsto f l (nhds C)) (hg : Tendsto g l atBot) : Tendsto (fun (x : β) => f x + g x) l 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_mul' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] {l : Filter β} {f g : β → α} {C : α} (hf : Tendsto f l atTop) (hg : Tendsto g l (nhds C)) : Tendsto (fun (x : β) => f x * g x) l atTop

In a linearly ordered 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.atTop_add {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [OrderTopology α] {l : Filter β} {f g : β → α} {C : α} (hf : Tendsto f l atTop) (hg : Tendsto g l (nhds C)) : Tendsto (fun (x : β) => f x + g x) l 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_mul' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] {l : Filter β} {f g : β → α} {C : α} (hf : Tendsto f l atBot) (hg : Tendsto g l (nhds C)) : Tendsto (fun (x : β) => f x * g x) l atBot

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

theorem Filter.Tendsto.atBot_add {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [OrderTopology α] {l : Filter β} {f g : β → α} {C : α} (hf : Tendsto f l atBot) (hg : Tendsto g l (nhds C)) : Tendsto (fun (x : β) => f x + g x) l 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_mabs_div_lt {α : Type u_1} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] [NoMaxOrder α] (a : α) : (nhds a).HasBasis (fun (ε : α) => 1 < ε) fun (ε : α) => {b : α | mabs (b / a) < ε}

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

theorem nhds_basis_Ioo_one_lt {α : Type u_1} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] [NoMaxOrder α] (a : α) : (nhds a).HasBasis (fun (ε : α) => 1 < ε) fun (ε : α) => Set.Ioo (a / ε) (a * ε)

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

theorem nhds_basis_Icc_one_lt {α : Type u_1} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] [NoMaxOrder α] [DenselyOrdered α] (a : α) : (nhds a).HasBasis (fun (x : α) => 1 < x) fun (ε : α) => Set.Icc (a / ε) (a * ε)

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

theorem nhds_basis_one_mabs_lt (α : Type u_1) [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] [NoMaxOrder α] : (nhds 1).HasBasis (fun (ε : α) => 1 < ε) fun (ε : α) => {b : α | mabs b < ε}

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

@[deprecated nhds_basis_zero_abs_lt (since := "2025-03-18")]

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

Alias of nhds_basis_zero_abs_lt.

theorem nhds_basis_Ioo_one_lt_of_one_lt {α : Type u_1} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] [NoMaxOrder α] {a : α} (ha : 1 < a) : (nhds a).HasBasis (fun (ε : α) => 1 < ε ∧ ε ≤ a) fun (ε : α) => Set.Ioo (a / ε) (a * ε)

If a > 1, then open intervals (a / ε, aε), 1 < ε ≤ a, form a basis of neighborhoods of a.

This upper bound for ε guarantees that all elements of these intervals are greater than one.

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

If a is positive, then the intervals (a - ε, a + ε), 0 < ε ≤ a, form a basis of neighborhoods of a.

This upper bound for ε guarantees that all elements of these intervals are positive.

theorem Set.OrdConnected.mem_nhdsGE {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {S : Set α} {x y : α} (hS : S.OrdConnected) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) : S ∈ nhdsWithin x (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_nhdsGT {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {S : Set α} {x y : α} (hS : S.OrdConnected) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) : S ∈ nhdsWithin x (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_nhdsLE {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {S : Set α} {x y : α} (hS : S.OrdConnected) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) : S ∈ nhdsWithin y (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_nhdsLT {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {S : Set α} {x y : α} (hS : S.OrdConnected) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) : S ∈ nhdsWithin y (Iio y)

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