Documentation

Mathlib.Topology.Order.LeftRightNhds

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:

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

@[deprecated TFAE_mem_nhdsGT (since := "2024-12-22")]

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

Alias of TFAE_mem_nhdsGT.

The following statements are equivalent:

s is a neighborhood of a within (a, +∞);
s is a neighborhood of a within (a, b];
s is a neighborhood of a within (a, b);
s includes (a, u) for some u ∈ (a, b];
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

@[deprecated mem_nhdsGT_iff_exists_mem_Ioc_Ioo_subset (since := "2024-12-22")]

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

Alias of mem_nhdsGT_iff_exists_mem_Ioc_Ioo_subset.

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.

@[deprecated mem_nhdsGT_iff_exists_Ioo_subset' (since := "2024-12-22")]

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

Alias of mem_nhdsGT_iff_exists_Ioo_subset'.

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)

@[deprecated nhdsGT_basis_of_exists_gt (since := "2024-12-22")]

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)

Alias of nhdsGT_basis_of_exists_gt.

theorem nhdsGT_basis {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] (a : α) :

(nhdsWithin a (Set.Ioi a)).HasBasis (fun (x : α) => a < x) (Set.Ioo a)

@[deprecated nhdsGT_basis (since := "2024-12-22")]

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)

Alias of nhdsGT_basis.

theorem nhdsGT_eq_bot_iff {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} :

nhdsWithin a (Set.Ioi a) = ⊥ ↔ IsTop a ∨ ∃ (b : α), a ⋖ b

@[deprecated nhdsGT_eq_bot_iff (since := "2024-12-22")]

theorem nhdsWithin_Ioi_eq_bot_iff {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} :

nhdsWithin a (Set.Ioi a) = ⊥ ↔ IsTop a ∨ ∃ (b : α), a ⋖ b

Alias of nhdsGT_eq_bot_iff.

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.

@[deprecated mem_nhdsGT_iff_exists_Ioo_subset (since := "2024-12-22")]

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

Alias of mem_nhdsGT_iff_exists_Ioo_subset.

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_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.

@[deprecated mem_nhdsGT_iff_exists_Ioc_subset (since := "2024-12-22")]

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

Alias of mem_nhdsGT_iff_exists_Ioc_subset.

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:

s is a neighborhood of b within (-∞, b)
s is a neighborhood of b within [a, b)
s is a neighborhood of b within (a, b)
s includes (l, b) for some l ∈ [a, b)
s includes (l, b) for some l < b

@[deprecated TFAE_mem_nhdsLT (since := "2024-12-22")]

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

Alias of TFAE_mem_nhdsLT.

The following statements are equivalent:

s is a neighborhood of b within (-∞, b)
s is a neighborhood of b within [a, b)
s is a neighborhood of b within (a, b)
s includes (l, b) for some l ∈ [a, b)
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

@[deprecated mem_nhdsLT_iff_exists_mem_Ico_Ioo_subset (since := "2024-12-22")]

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

Alias of mem_nhdsLT_iff_exists_mem_Ico_Ioo_subset.

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.

@[deprecated mem_nhdsLT_iff_exists_Ioo_subset' (since := "2024-12-22")]

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

Alias of mem_nhdsLT_iff_exists_Ioo_subset'.

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.

@[deprecated mem_nhdsLT_iff_exists_Ioo_subset (since := "2024-12-22")]

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

Alias of mem_nhdsLT_iff_exists_Ioo_subset.

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.

@[deprecated mem_nhdsLT_iff_exists_Ico_subset (since := "2024-12-22")]

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

Alias of mem_nhdsLT_iff_exists_Ico_subset.

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

@[deprecated nhdsLT_basis_of_exists_lt (since := "2024-12-22")]

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

Alias of nhdsLT_basis_of_exists_lt.

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

@[deprecated nhdsLT_basis (since := "2024-12-22")]

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

Alias of nhdsLT_basis.

theorem nhdsLT_eq_bot_iff {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} :

nhdsWithin a (Set.Iio a) = ⊥ ↔ IsBot a ∨ ∃ (b : α), b ⋖ a

@[deprecated nhdsLT_eq_bot_iff (since := "2024-12-22")]

theorem nhdsWithin_Iio_eq_bot_iff {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} :

nhdsWithin a (Set.Iio a) = ⊥ ↔ IsBot a ∨ ∃ (b : α), b ⋖ a

Alias of nhdsLT_eq_bot_iff.

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:

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

@[deprecated TFAE_mem_nhdsGE (since := "2024-12-22")]

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

Alias of TFAE_mem_nhdsGE.

The following statements are equivalent:

s is a neighborhood of a within [a, +∞);
s is a neighborhood of a within [a, b];
s is a neighborhood of a within [a, b);
s includes [a, u) for some u ∈ (a, b];
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

@[deprecated mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset (since := "2024-12-22")]

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

Alias of mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset.

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.

@[deprecated mem_nhdsGE_iff_exists_Ico_subset' (since := "2024-12-22")]

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

Alias of mem_nhdsGE_iff_exists_Ico_subset'.

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.

@[deprecated mem_nhdsGE_iff_exists_Ico_subset (since := "2024-12-22")]

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

Alias of mem_nhdsGE_iff_exists_Ico_subset.

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)

@[deprecated nhdsGE_basis_Ico (since := "2024-12-22")]

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)

Alias of nhdsGE_basis_Ico.

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.

@[deprecated nhdsGE_basis_Icc (since := "2024-12-22")]

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)

Alias of nhdsGE_basis_Icc.

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.

@[deprecated mem_nhdsGE_iff_exists_Icc_subset (since := "2024-12-22")]

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

Alias of mem_nhdsGE_iff_exists_Icc_subset.

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:

s is a neighborhood of b within (-∞, b]
s is a neighborhood of b within [a, b]
s is a neighborhood of b within (a, b]
s includes (l, b] for some l ∈ [a, b)
s includes (l, b] for some l < b

@[deprecated TFAE_mem_nhdsLE (since := "2024-12-22")]

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

Alias of TFAE_mem_nhdsLE.

The following statements are equivalent:

s is a neighborhood of b within (-∞, b]
s is a neighborhood of b within [a, b]
s is a neighborhood of b within (a, b]
s includes (l, b] for some l ∈ [a, b)
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

@[deprecated mem_nhdsLE_iff_exists_mem_Ico_Ioc_subset (since := "2024-12-22")]

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

Alias of mem_nhdsLE_iff_exists_mem_Ico_Ioc_subset.

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.

@[deprecated mem_nhdsLE_iff_exists_Ioc_subset' (since := "2024-12-22")]

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

Alias of mem_nhdsLE_iff_exists_Ioc_subset'.

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.

@[deprecated mem_nhdsLE_iff_exists_Ioc_subset (since := "2024-12-22")]

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

Alias of mem_nhdsLE_iff_exists_Ioc_subset.

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.

@[deprecated mem_nhdsLE_iff_exists_Icc_subset (since := "2024-12-22")]

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

Alias of mem_nhdsLE_iff_exists_Icc_subset.

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.

@[deprecated nhdsLE_basis_Icc (since := "2024-12-22")]

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

Alias of nhdsLE_basis_Icc.

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.

@[deprecated Set.OrdConnected.mem_nhdsGE (since := "2024-12-22")]

theorem Set.OrdConnected.mem_nhdsWithin_Ici {α : 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)

Alias of Set.OrdConnected.mem_nhdsGE.

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.

@[deprecated Set.OrdConnected.mem_nhdsGT (since := "2024-12-22")]

theorem Set.OrdConnected.mem_nhdsWithin_Ioi {α : 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)

Alias of Set.OrdConnected.mem_nhdsGT.

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.

@[deprecated Set.OrdConnected.mem_nhdsLE (since := "2024-12-22")]

theorem Set.OrdConnected.mem_nhdsWithin_Iic {α : 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)

Alias of Set.OrdConnected.mem_nhdsLE.

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.

@[deprecated Set.OrdConnected.mem_nhdsLT (since := "2024-12-22")]

theorem Set.OrdConnected.mem_nhdsWithin_Iio {α : 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)

Alias of Set.OrdConnected.mem_nhdsLT.

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