countable_setOf_isolated_left
theorem countable_setOf_isolated_left :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : SecondCountableTopology α], {x | nhdsWithin x (Set.Iio x) = ⊥}.Countable
The theorem `countable_setOf_isolated_left` states that in any second-countable topological space, which is also a linearly ordered space with an order topology, the set of points for which the "neighborhood within" filter (`nhdsWithin`), when applied to a left-infinite right-open interval (`Set.Iio`), yields the bottom filter (`⊥`), is countable. In other words, it says that the set of points which are isolated on their left side is countable in any second-countable linearly ordered space with an order topology.
More concisely: In a second-countable, linearly ordered space with an order topology, the set of points with only left-isolated neighbors is countable.
|
mem_nhdsWithin_Iic_iff_exists_Icc_subset
theorem mem_nhdsWithin_Iic_iff_exists_Icc_subset :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : NoMinOrder α] [inst_4 : DenselyOrdered α] {a : α} {s : Set α},
s ∈ nhdsWithin a (Set.Iic a) ↔ ∃ l < a, Set.Icc l a ⊆ s
This theorem states that for any set 's' of a type 'α', which is endowed with a topological space, a linear order, an order topology, a property that there is no minimum element, and the property of being densely ordered, 's' is a neighborhood of a point 'a' within the interval from negative infinity to 'a' inclusive (`(-∞, a]`) if and only if there exists a real number 'l' less than 'a' such that the closed interval from 'l' to 'a' is a subset of 's'. In other words, 's' is close to 'a' within `(-∞, a]` if and only if 's' contains an interval `[l, a]` where 'l' is strictly less than 'a'.
More concisely: For a set endowed with a topological space, a linear order, an order topology, no minimum element, and dense ordering, it is equal to the neighborhood of a point in the interval from negative infinity to that point if and only if it contains an interval with a strictly smaller element.
|
mem_nhdsWithin_Iio_iff_exists_Ioo_subset
theorem mem_nhdsWithin_Iio_iff_exists_Ioo_subset :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : NoMinOrder α] {a : α} {s : Set α}, s ∈ nhdsWithin a (Set.Iio a) ↔ ∃ l ∈ Set.Iio a, Set.Ioo l a ⊆ s
This theorem states that for any given type `α` equipped with a topological space structure, a linear order, an order topology, and no minimal order, and for any element `a` of `α` and any set `s` of `α`, the set `s` is a neighborhood of `a` within the interval `(-∞, a)` if and only if there exists some `l` in `(-∞, a)`, such that the open interval `(l, a)` is a subset of `s`.
More concisely: For any topological space `(α, top)` with a linear order and no minimal element, and for any `a` in `α` and set `s` containing `a`, `s` is a neighborhood of `a` within the interval `(-∞, a)` if and only if there exists an `l` in `(-∞, a)` such that the open interval `(l, a)` is a subset of `s`.
|
mem_nhdsWithin_Iic_iff_exists_Ioc_subset'
theorem mem_nhdsWithin_Iic_iff_exists_Ioc_subset' :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α] {a l' : α}
{s : Set α}, l' < a → (s ∈ nhdsWithin a (Set.Iic a) ↔ ∃ l ∈ Set.Iio a, Set.Ioc l a ⊆ s)
This theorem states that for any types `α`, where `α` forms a topological space, a linear order, and an order topology, and for any elements `a`, `l'`, and set `s` in `α`, if `l'` is less than `a`, then `s` is a neighborhood of `a` within the set `(-∞, a]` if and only if there exists an element `l` in the set `(-∞, a)` such that the interval `(l, a]` is a subset of `s`. This condition is provided that `a` is not a bottom element in the linear order.
More concisely: For any topological space, linear order, and order topology on type `α`, if `a` is an element with no bottom element, then `s` is a neighborhood of `a` if and only if there exists `l` in `(-∞, a)` such that `(l, a] ⊆ s`.
|
TFAE_mem_nhdsWithin_Iic
theorem TFAE_mem_nhdsWithin_Iic :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α] {a b : α},
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 theorem `TFAE_mem_nhdsWithin_Iic` states that for a topological space with a linear order and an order topology, and for any two elements `a` and `b` such that `a < b`, the following five statements about a set `s` are equivalent:
0. `s` is a neighborhood of `b` within the interval `(-∞, b]` (i.e., `s` contains all points in this interval sufficiently close to `b`).
1. `s` is a neighborhood of `b` within the closed interval `[a, b]`.
2. `s` is a neighborhood of `b` within the half-open interval `(a, b]`.
3. There exists an element `l` in the half-open interval `[a, b)` such that the half-open interval `(l, b]` is included in `s`.
4. There exists an element `l` less than `b` such that the half-open interval `(l, b]` is included in `s`.
The `TFAE` in the theorem name stands for "the following are equivalent". This means that if any one of these statements is true, then all the others are also true, and vice versa.
More concisely: For a topological space with a linear order and an order topology, the sets that are neighborhoods of an element `b` within the interval `(-∞, b]`, the closed interval `[a, b]`, and the half-open interval `(a, b]` are equivalent, as are the sets with an element `l` in the half-open interval `[a, b)` or less than `b` such that `(l, b]` is included in the set.
|
mem_nhdsWithin_Ioi_iff_exists_Ioo_subset'
theorem mem_nhdsWithin_Ioi_iff_exists_Ioo_subset' :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α] {a u' : α}
{s : Set α}, a < u' → (s ∈ nhdsWithin a (Set.Ioi a) ↔ ∃ u ∈ Set.Ioi a, Set.Ioo a u ⊆ s)
This theorem states that for any type `α` equipped with a topological space structure, a linear order structure, and an order topology structure, and given any elements `a` and `u'` of `α` and a set `s` of `α`, if `a` is smaller than `u'`, then `s` is a neighborhood of `a` within the interval `(a, +∞)` if and only if there exists an element `u` in the interval `(a, +∞)` such that the open interval `(a, u)` is a subset of `s`. This is under the condition that `a` is not a top element in the order. Here, the interval `(a, +∞)` is a set of elements greater than `a` and the interval `(a, u)` is a set of elements that are strictly between `a` and `u`.
More concisely: For any type `α` with topological space, linear order, and order topology structures, if `a` is a non-top element in `α`, then `s` is a neighborhood of `a` within the interval `(a, +∞)` if and only if there exists an `u` in `(a, +∞)` such that `(a, u) ⊆ s`.
|
TFAE_mem_nhdsWithin_Iio
theorem TFAE_mem_nhdsWithin_Iio :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α] {a b : α},
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 theorem states that for any topological space, endowed with a linear order and an order topology, and given any two elements `a` and `b` in this space with `a` less than `b`, the following five conditions are equivalent for a set `s`:
1. `s` is a neighborhood of `b` within the interval `(-∞, b)`.
2. `s` is a neighborhood of `b` within the interval `[a, b)`.
3. `s` is a neighborhood of `b` within the interval `(a, b)`.
4. `s` includes the open interval `(l, b)` for some `l` in the closed-open interval `[a, b)`.
5. `s` includes the open interval `(l, b)` for some `l` less than `b`.
Here, a neighborhood of `b` within a set is a set which contains `b` and has some open set around `b` that is entirely contained within the set. An interval `(a, b)` is the set of all elements strictly between `a` and `b`, while `[a, b)` includes `a` but not `b`. The notation `(-∞, b)` refers to all elements less than `b`.
More concisely: For any element `b` in a topological space endowed with a linear order and order topology, and any `a` such that `a < b`, sets `s` are equivalent if and only if they are neighborhoods of `b` in the intervals `(a, b)`, `[a, b)`, `(-\infty, b)`, or `(l, b)` for some `l < b`.
|
nhds_basis_Ioo_pos
theorem nhds_basis_Ioo_pos :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrderedAddCommGroup α] [inst_2 : OrderTopology α]
[inst_3 : NoMaxOrder α] (a : α), (nhds a).HasBasis (fun ε => 0 < ε) fun ε => Set.Ioo (a - ε) (a + ε)
The theorem `nhds_basis_Ioo_pos` states that for any type `α` that is a topological space, a linearly ordered additive commutative group, has an order topology, and has no maximum order, and for any element `a` of type `α`, the neighborhood filter `nhds a` has a basis consisting of open intervals of the form `(a - ε, a + ε)`, where `ε` is a positive real number. In other words, every neighborhood of `a` contains an open interval `(a - ε, a + ε)` for some positive `ε`, and every such interval is a neighborhood of `a`.
More concisely: If `α` is a topological space, a linearly ordered additive commutative group with no maximum order, then for any `a` in `α`, the neighborhood filter of `a` has a basis consisting of open intervals `(a - ε, a + ε)` for some positive real number `ε`.
|
TFAE_mem_nhdsWithin_Ioi
theorem TFAE_mem_nhdsWithin_Ioi :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α] {a b : α},
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
This theorem states that for a given set `s` and two elements `a` and `b` such that `a < b` in a topological space `α` that also has a linear order and an order topology, the following statements are equivalent:
0. `s` is a neighborhood of `a` within the interval `(a, +∞)`.
1. `s` is a neighborhood of `a` within the closed interval `(a, b]`.
2. `s` is a neighborhood of `a` within the open interval `(a, b)`.
3. `s` includes the open interval `(a, u)` for some `u` in the interval `(a, b]`.
4. `s` includes the open interval `(a, u)` for some `u` that is greater than `a`.
In other words, these conditions can be used interchangeably in theorems involving neighborhoods within intervals.
More concisely: In a topological space with a linear order and an order topology, the neighborhoods of an element `a` with strict inequality to another element `b` are equivalent: `(a < b) => { (a is a neighborhood of a in (a, +∞)), (a is a neighborhood of a in (a, b]), (a is a neighborhood of a in (a, b) and s includes some open interval (a, u) for some `u` in (a, b]) } => (a is a neighborhood of a in (a, b) and s includes some open interval (a, u) for some `u` > a)`.
|
mem_nhdsWithin_Ioi_iff_exists_Ioc_subset
theorem mem_nhdsWithin_Ioi_iff_exists_Ioc_subset :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : NoMaxOrder α] [inst_4 : DenselyOrdered α] {a : α} {s : Set α},
s ∈ nhdsWithin a (Set.Ioi a) ↔ ∃ u ∈ Set.Ioi a, Set.Ioc a u ⊆ s
This theorem states that for any type `α` that forms a topological space, has a linear order, has a topological order, has no maximum order, and is densely ordered, and any element `a` of type `α` and set `s` of elements of type `α`, `s` is a neighborhood of `a` within the interval `(a, +∞)` if and only if there exists an element `u` in `(a, +∞)` such that the interval `(a, u]` is a subset of `s`. Here, the interval `(a, +∞)` represents all elements greater than `a` and the interval `(a, u]` represents all elements strictly greater than `a` and less than or equal to `u`.
More concisely: For any densely ordered, no maxima topological space `α`, an element `a` in `α` and a set `s` of elements in `α`, `s` is a neighborhood of `a` within the interval `(a, +∞)` if and only if there exists `u` in `(a, +∞)` such that `(a, u] ⊆ s`.
|
Filter.Tendsto.atTop_add
theorem Filter.Tendsto.atTop_add :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrderedAddCommGroup α]
[inst_2 : OrderTopology α] {l : Filter β} {f g : β → α} {C : α},
Filter.Tendsto f l Filter.atTop →
Filter.Tendsto g l (nhds C) → Filter.Tendsto (fun x => f x + g x) l Filter.atTop
This theorem states that, in a linearly ordered additive commutative group equipped with the order topology, if a function `f` tends towards infinity (represented as `atTop`) and another function `g` tends towards a constant `C`, then the pointwise sum of `f` and `g` also tends towards infinity. In terms of filters, the pre-image of any neighborhood of infinity under `f` and of `C` under `g` are both neighborhoods with respect to a certain filter `l`, implying that the pre-image of any neighborhood of infinity under the sum function (`f` + `g`) is also a neighborhood with respect to `l`. In other words, the sum of a function that tends to infinity and a function that tends to a constant itself tends to infinity.
More concisely: If `f` tends to infinity and `g` tends to a constant in a linearly ordered additive commutative group, then `f + g` also tends to infinity.
|
mem_nhdsWithin_Iio_iff_exists_Ioo_subset'
theorem mem_nhdsWithin_Iio_iff_exists_Ioo_subset' :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α] {a l' : α}
{s : Set α}, l' < a → (s ∈ nhdsWithin a (Set.Iio a) ↔ ∃ l ∈ Set.Iio a, Set.Ioo l a ⊆ s)
The theorem `mem_nhdsWithin_Iio_iff_exists_Ioo_subset'` asserts that for any type `α` that has a topological space structure, a linear order, and an order topology, and for any elements `a` and `l'` of type `α` and a set `s` of type `α`, if `l'` is less than `a`, then `s` is a neighborhood of `a` within the set of elements less than `a` (`(-∞, a)`) if and only if there exists an element `l` less than `a` such that the open interval from `l` to `a` (`(l, a)`) is a subset of `s`. Here, a "neighborhood of `a` within `(-∞, a)`" is a set that contains the intersection of `(-∞, a)` and a neighborhood of `a`, and an "open interval from `l` to `a`" is the set of elements that are greater than `l` and less than `a`.
More concisely: For any topological space with a linear order and order topology, an element `a` has a neighborhood `s` within the set of elements less than `a` if and only if there exists an element `l` less than `a` such that the open interval `(l, a)` is a subset of `s`.
|
mem_nhdsWithin_Ici_iff_exists_Ico_subset
theorem mem_nhdsWithin_Ici_iff_exists_Ico_subset :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : NoMaxOrder α] {a : α} {s : Set α}, s ∈ nhdsWithin a (Set.Ici a) ↔ ∃ u ∈ Set.Ioi a, Set.Ico a u ⊆ s
This theorem states that, given a topological space with an associated linear order and order topology, and assuming there is no maximum order element, a set `s` is a neighborhood of a point `a` within the closed-interval `[a, +∞)`, if and only if there exists an element `u` in the open-interval `(a, +∞)` such that the half-open interval `[a, u)` is a subset of `s`. In other words, `s` is considered a local neighborhood of `a` in the set of all elements greater than or equal to `a` if it contains a half-open interval starting at `a` and extending to some element `u` that is strictly greater than `a`.
More concisely: A set is a neighborhood of a point in a topological space with an associated linear order if and only if it contains a half-open interval starting at that point and extending to some strictly greater element.
|
mem_nhdsWithin_Ioi_iff_exists_Ioo_subset
theorem mem_nhdsWithin_Ioi_iff_exists_Ioo_subset :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : NoMaxOrder α] {a : α} {s : Set α}, s ∈ nhdsWithin a (Set.Ioi a) ↔ ∃ u ∈ Set.Ioi a, Set.Ioo a u ⊆ s
The theorem `mem_nhdsWithin_Ioi_iff_exists_Ioo_subset` asserts the equivalence between a set `s` being a neighborhood of a point `a` within the interval `(a, +∞)` and the existence of an interval `(a, u)` with `a < u` fully contained in the set `s`. In particular, in the context of a topological space with a linear order and order topology where there is no maximum order, the theorem posits that `s` is in the intersection of the neighborhood filter of `a` and the principal filter of the interval `(a, +∞)` if and only if there exists a `u` in the interval `(a, +∞)` such that the interval `(a, u)` is a subset of `s`.
More concisely: A set `s` contains a neighborhood of `a` within the interval `(a, +∞)` if and only if there exists a `u` in `(a, +∞)` such that `(a, u)` is a subset of `s`.
|
Filter.Tendsto.atBot_add
theorem Filter.Tendsto.atBot_add :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrderedAddCommGroup α]
[inst_2 : OrderTopology α] {l : Filter β} {f g : β → α} {C : α},
Filter.Tendsto f l Filter.atBot →
Filter.Tendsto g l (nhds C) → Filter.Tendsto (fun x => f x + g x) l Filter.atBot
This theorem states that in a linearly ordered additive commutative group equipped with the order topology, if a function `f` tends towards negative infinity (`atBot`), and another function `g` tends towards a constant `C`, then the function formed by the pointwise addition of `f` and `g` also tends towards negative infinity. The limit behavior of these functions is evaluated with respect to some arbitrary filter `l`.
More concisely: In a linearly ordered additive commutative group with the order topology, if function `f` converges to negative infinity and function `g` converges to a constant `C` with respect to some filter `l`, then the function `f + g` converges to negative infinity.
|
mem_nhdsWithin_Iic_iff_exists_Ioc_subset
theorem mem_nhdsWithin_Iic_iff_exists_Ioc_subset :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : NoMinOrder α] {a : α} {s : Set α}, s ∈ nhdsWithin a (Set.Iic a) ↔ ∃ l ∈ Set.Iio a, Set.Ioc l a ⊆ s
This theorem states that in the context of a topological space, a linear order, an order topology, and a no minimum order, for any given set 's' and element 'a', 's' is considered a "neighborhood within" the interval `(-∞, a]` (denoted as `nhdsWithin a (Set.Iic a)`) if and only if there exists an element 'l' such that 'l' is less than 'a' and the interval `(l, a]` (denoted as `Set.Ioc l a`) is a subset of 's'. The term "neighborhood within" refers to sets that contain the intersection of 's' and a neighborhood of 'a'.
More concisely: A set 's' is a neighborhood within the interval `(-∞, a]` in a topological space with a no minimum order if and only if there exists an element 'l' < 'a' such that the interval `(l, a]` is a subset of 's'.
|
nhds_basis_Ioo_pos_of_pos
theorem nhds_basis_Ioo_pos_of_pos :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrderedAddCommGroup α] [inst_2 : OrderTopology α]
[inst_3 : NoMaxOrder α] {a : α},
0 < a → (nhds a).HasBasis (fun ε => 0 < ε ∧ ε ≤ a) fun ε => Set.Ioo (a - ε) (a + ε)
This theorem states that for any type `α` that is a topological space, a linear ordered additive commutative group, has an order topology, and does not have a maximum order, if `a` is a positive element of `α`, then we can form a basis for the neighborhood filter around `a` using left-open right-open intervals (`Set.Ioo`). Specifically, the basis consists of those intervals `(a - ε, a + ε)` where `ε` is a positive real number not greater than `a`. The neighborhood filter is a concept in topology that contains all possible neighborhoods (sets containing an open set) around a point.
More concisely: For any topological space, additive commutative group with order topology and no maximum element, given a positive element `a`, the set of left-open right-open intervals `(a - ε, a + ε)` with `ε < a` forms a basis for the neighborhood filter around `a`.
|
Filter.Tendsto.add_atTop
theorem Filter.Tendsto.add_atTop :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrderedAddCommGroup α]
[inst_2 : OrderTopology α] {l : Filter β} {f g : β → α} {C : α},
Filter.Tendsto f l (nhds C) →
Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x + g x) l Filter.atTop
The theorem states that in a topological space, which is also a linearly ordered additive commutative group with an order topology, if a function `f` tends towards a certain value `C`, and another function `g` tends towards infinity (`atTop`), then the sum of the two functions `f + g` also tends towards infinity. This means that if for every neighborhood of `C`, the pre-image of `f` is a neighborhood in the filter `l`, and for every set of numbers greater than a certain value, the pre-image of `g` is also a neighborhood in `filter l`, then for every set of numbers greater than a certain value, the pre-image of `f + g` will also be a neighborhood in `filter l`.
More concisely: In a topological group with an order topology, if a function `f` converges to a limit `C` and another function `g` goes to infinity, then their sum `f + g` also goes to infinity.
|
nhds_basis_abs_sub_lt
theorem nhds_basis_abs_sub_lt :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrderedAddCommGroup α] [inst_2 : OrderTopology α]
[inst_3 : NoMaxOrder α] (a : α), (nhds a).HasBasis (fun ε => 0 < ε) fun ε => {b | |b - a| < ε}
This theorem, named `nhds_basis_abs_sub_lt`, states that for any type `α` that is a topological space, a linear ordered additive commutative group, an order topology, and has no maximum order, and for any element `a` of type `α`, the neighborhood filter of `a` (`nhds a`) has a basis consisting of sets `{b | |b - a| < ε}` where `ε` is a positive real number. In simpler terms, every neighborhood of `a` contains an open set of points `b` whose absolute difference from `a` is less than some positive number `ε`.
More concisely: For any topological space `α` that is a linear ordered additive commutative group without a maximum order, the neighborhood filter of any element `a` in `α` has a basis consisting of open sets `{b : α | |b - a| < ε}` for some positive real number `ε`.
|
nhdsWithin_Iic_basis_Icc
theorem nhdsWithin_Iic_basis_Icc :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : NoMinOrder α] [inst_4 : DenselyOrdered α] {a : α},
(nhdsWithin a (Set.Iic a)).HasBasis (fun x => x < a) fun x => Set.Icc x a
This theorem states that for any point `a` in a densely ordered, topological space with a linear order that has no minimum element and an order topology, the filter of neighborhoods within the set of all elements less than or equal to `a` (`nhdsWithin a (Set.Iic a)`) has a basis consisting of closed intervals (`Set.Icc x a`). Each of these closed intervals is indexed by elements `x` that are less than `a`. In mathematical terms, this means that we can generate all neighborhoods of `a` within the set of elements less than or equal to `a` by considering all closed intervals [x, a], where x is less than a.
More concisely: In a densely ordered, topological space with a linear order and no minimum element, the filter of neighborhoods of any point `a` within the set of elements less than or equal to `a` has a basis consisting of closed intervals `[x, a]` for all `x` less than `a`.
|
nhdsWithin_Ici_basis_Icc
theorem nhdsWithin_Ici_basis_Icc :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : NoMaxOrder α] [inst_4 : DenselyOrdered α] {a : α},
(nhdsWithin a (Set.Ici a)).HasBasis (fun x => a < x) (Set.Icc a)
This theorem states that for any type `α` that is a topological space, has a linear order, is an order topology, has no maximum order, and is densely ordered, and for any `a` in `α`, the filter of right neighborhoods (i.e., the sets containing the intersection of a right-infinite interval starting at `a` and a neighborhood of `a`) has a basis of left-closed right-closed intervals. The predicate to generate the basis is "is greater than `a`", and the sets in the basis are the closed intervals from `a` to each element that is greater than `a`.
More concisely: For any densely ordered, no maxima, linearly ordered topological space `α` without a maximum, the filter of right neighborhoods of an element `a` in `α` has a basis of left-closed right-closed intervals generated by elements strictly greater than `a`.
|
countable_setOf_isolated_right
theorem countable_setOf_isolated_right :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : SecondCountableTopology α], {x | nhdsWithin x (Set.Ioi x) = ⊥}.Countable
The theorem states that for any type `α` which is a topological space, has a linear order, an order topology and a second-countable topology, the set of points which are isolated on the right is countable. A point is considered to be isolated on the right if the neighborhood within the right-infinite interval starting from the point (i.e., the set of all points greater than the given point) is empty. This is expressed in Lean as `nhdsWithin x (Set.Ioi x) = ⊥` where `Set.Ioi x` represents the right-infinite interval starting from `x`, and `nhdsWithin x (Set.Ioi x)` is the filter representing the intersection of this interval and a neighborhood of `x`. If this filter is equal to the bottom element `⊥`, it means the intersection is empty, indicating the point `x` is isolated on the right. The theorem states that under the given conditions, the set of all such isolated points is countable.
More concisely: Given a topological space `α` with a linear order, an order topology, and a second-countable topology, the set of isolated points on the right is countable.
|
TFAE_mem_nhdsWithin_Ici
theorem TFAE_mem_nhdsWithin_Ici :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α] {a b : α},
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
This theorem states that for any topological space with a linear order and order topology, and given two elements 'a' and 'b' of this space with 'a' less than 'b', the following statements are equivalent for any set 's':
0. 's' is a neighborhood of 'a' within the interval from 'a' to positive infinity.
1. 's' is a neighborhood of 'a' within the closed interval from 'a' to 'b'.
2. 's' is a neighborhood of 'a' within the half-open interval from 'a' to 'b'.
3. 's' includes the half-open interval from 'a' to some 'u' in the open-closed interval from 'a' to 'b'.
4. 's' includes the half-open interval from 'a' to some 'u' greater than 'a'.
A neighborhood of 'a' within a set is a set containing the intersection of a neighborhood of 'a' and the set. In this context, intervals are sets of elements depending on the relation between the element and the endpoints 'a' and 'b'.
More concisely: In a topological space with a linear order and order topology, for any element 'a' less than 'b', the sets that are neighborhoods of 'a' within the interval from 'a' to positive infinity, the closed interval from 'a' to 'b', the half-open interval from 'a' to 'b', and the half-open interval from 'a' to some 'u' in the open-closed interval from 'a' to 'b' are equivalent.
|
mem_nhdsWithin_Iio_iff_exists_Ico_subset
theorem mem_nhdsWithin_Iio_iff_exists_Ico_subset :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : NoMinOrder α] [inst_4 : DenselyOrdered α] {a : α} {s : Set α},
s ∈ nhdsWithin a (Set.Iio a) ↔ ∃ l ∈ Set.Iio a, Set.Ico l a ⊆ s
This theorem states that for any type `α` equipped with a topological space structure, a linear order, an order topology, a property that there is no minimum element (`NoMinOrder`) and a densely ordered property, for any element 'a' of type `α` and any set `s` of type `α`, `s` is a neighborhood of `a` within the open interval `(-∞, a)` if and only if there exists an element `l` in `(-∞, a)` such that the closed-open interval `[l, a)` is a subset of `s`. In other words, `s` is near `a` in the context of all elements less than `a` if and only if we can find a left-closed right-open interval ending at `a` that is entirely contained within `s`.
More concisely: For any densely ordered, no minima topological space `(α, top)`, an element `a` in `α`, and a set `s` in `α`, `s` is a neighborhood of `a` if and only if there exists `l in (-\infty, a)` such that `[l, a)` is a subset of `s` in the order topology.
|
mem_nhdsWithin_Ici_iff_exists_Icc_subset
theorem mem_nhdsWithin_Ici_iff_exists_Icc_subset :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : NoMaxOrder α] [inst_4 : DenselyOrdered α] {a : α} {s : Set α},
s ∈ nhdsWithin a (Set.Ici a) ↔ ∃ u, a < u ∧ Set.Icc a u ⊆ s
This theorem states that for any type `α` that has a topological space structure, a linear order, an order topology, no maximum order, and is densely ordered, a set `s` of elements of this type is a neighborhood of an element `a` within the interval `[a, +∞)` if and only if there exists an element `u` such that `a` is less than `u` and the closed interval `[a, u]` is a subset of `s`. In the context of topology and set theory, a neighborhood within a set is a concept that generalizes the notion of an open set. In this case, the theorem is specifying when a set is considered a neighborhood of a specific point `a` within the interval from `a` to positive infinity.
More concisely: For a densely ordered type `α` with order topology, having no maximum order and no maximum element, a set `s` is a neighborhood of `a` in the interval `[a, +∞)` if and only if there exists `u` in `α` such that `a < u` and `[a, u]` is a subset of `s`.
|
mem_nhdsWithin_Ici_iff_exists_Ico_subset'
theorem mem_nhdsWithin_Ici_iff_exists_Ico_subset' :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α] {a u' : α}
{s : Set α}, a < u' → (s ∈ nhdsWithin a (Set.Ici a) ↔ ∃ u ∈ Set.Ioi a, Set.Ico a u ⊆ s)
This theorem states that, given a topological space with a linear ordering and an order topology, along with elements `a` and `u'` of the space and a set `s` in this space such that `a < u'`, then `s` is a neighborhood of `a` within the interval `[a, +∞)` if and only if there exists an element `u` in the open interval `(a, +∞)` such that the closed-open interval `[a, u)` is a subset of `s`. Here, a neighborhood of `a` within `[a, +∞)` is a set containing the intersection of `[a, +∞)` and a neighborhood of `a`. The intervals are defined with respect to the linear ordering: `[a, +∞)` contains all elements greater than or equal to `a`, `(a, +∞)` contains all elements strictly greater than `a`, and `[a, u)` contains all elements `x` such that `a ≤ x < u`.
More concisely: A set `s` is a neighborhood of `a` in the order topology of a linear ordered topological space if and only if there exists an element `u` in the open interval `(a, +∞)` such that `[a, u) ⊆ s`.
|
nhds_eq_iInf_abs_sub
theorem nhds_eq_iInf_abs_sub :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrderedAddCommGroup α] [inst_2 : OrderTopology α]
(a : α), nhds a = ⨅ r, ⨅ (_ : r > 0), Filter.principal {b | |a - b| < r}
This theorem states that for any type `α` that is a topological space, a linear ordered additive commutative group, and whose order induces the topology (this is generally the case for the real numbers, for example), the neighborhood filter at a point `a` (denoted `nhds a`) is equal to the infimum of the principal filters of all sets of the form `{b | |a - b| < r}`, for all positive `r`. In simpler terms, it is saying that the neighborhoods of a point in such a space can be generated by considering all the sets of points that are within a certain positive distance `r` from the point, and taking the infimum of (i.e., the smallest filter containing) the collections of all sets that contain these sets. This is an important concept in topology, as it captures the idea of 'closeness' in a rigorous way.
More concisely: For any topological space `α` that is a linear ordered additive commutative group with the order inducing the topology, the neighborhood filter at a point `a` equals the infimum of the principal filters of all open balls centered at `a` with positive radius.
|
Filter.Tendsto.add_atBot
theorem Filter.Tendsto.add_atBot :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrderedAddCommGroup α]
[inst_2 : OrderTopology α] {l : Filter β} {f g : β → α} {C : α},
Filter.Tendsto f l (nhds C) →
Filter.Tendsto g l Filter.atBot → Filter.Tendsto (fun x => f x + g x) l Filter.atBot
The theorem states that in a linearly ordered additive commutative group with the order topology, if a function `f` tends towards a constant `C` and another function `g` tends towards negative infinity (`atBot`), then the function resulting from their addition (`f + g`) also tends towards negative infinity (`atBot`). This behavior is evaluated under a filter `l`, and the theorem asserts that this is true for all such `f`, `g`, `C`, and `l` satisfying the given conditions.
More concisely: In a linearly ordered additive commutative group with the order topology, if function `f` converges to a constant `C` and function `g` converges to negative infinity under filter `l`, then their sum `f + g` converges to negative infinity under filter `l`.
|