nhdsWithin_Iic_basis'
theorem nhdsWithin_Iic_basis' :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α] {a : α},
(∃ l, l < a) → (nhdsWithin a (Set.Iic a)).HasBasis (fun l => l < a) fun l => Set.Ioc l a
This theorem states that for any type `α` endowed with a topological space structure, a linear order structure, and an order topology structure, and for a given element `a` from `α`, if there exists an element `l` less than `a`, then the filter of neighborhoods within `Set.Iic a` (the set of all values less than or equal to `a`) at `a` has a basis indexed by elements less than `a`, with each basis element being the left-open right-closed interval `Set.Ioc l a` (the set of all values greater than `l` and less than or equal to `a`).
In simpler terms, this theorem provides a way to generate a basis for the neighborhood filter around a point `a` in a topological space, specifically within the set of all points less than or equal to `a`, by using open-closed intervals that end at `a` and begin from any point less than `a`.
More concisely: For any topological space `(α, top)` endowed with a linear order `≤` and for any element `a ∈ α` with a predecessor `l`, the filter basis of neighborhoods at `a` within `Set.Iic a` is given by the collection of left-open right-closed intervals `Set.Ioc l a`.
|
StrictMono.embedding_of_ordConnected
theorem StrictMono.embedding_of_ordConnected :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] [inst_2 : TopologicalSpace α]
[h : OrderTopology α] [inst_3 : TopologicalSpace β] [inst_4 : OrderTopology β] {f : α → β},
StrictMono f → (Set.range f).OrdConnected → Embedding f
The theorem `StrictMono.embedding_of_ordConnected` states that for any two types `α` and `β`, given that `α` and `β` have a linear ordering and topological space structure, and are equipped with order topology, if a function `f` from `α` to `β` is strictly monotone and the range of `f` is order-connected - which means every value between any two values in the range is also in the range - then `f` is a topological embedding. A topological embedding is a function between topological spaces that is homeomorphic to its image, meaning it preserves the topological structure.
More concisely: A strictly monotone function between order-connected, linearly ordered types with order topology is a topological embedding.
|
countable_of_isolated_right'
theorem countable_of_isolated_right' :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst : SecondCountableTopology α], {x | ∃ y, x < y ∧ Set.Ioo x y = ∅}.Countable
This theorem states that in a second-countable topological space, which also has a linear order and an order topology, the set of points which are isolated on the right is countable. A point is said to be isolated on the right if there exists a point 'y' such that 'x' is less than 'y' and the open interval `(x, y)` is empty. In other words, there's a 'gap' immediately to the right of 'x'. 'Second-countable' means that the topology has a countable base, i.e., it can be generated by a countable collection of open sets.
More concisely: In a second-countable topological space with a linear order and order topology, the set of points isolated on the right is countable.
|
OrderTopology.topology_eq_generate_intervals
theorem OrderTopology.topology_eq_generate_intervals :
∀ {α : Type u_1} [t : TopologicalSpace α] [inst : Preorder α] [self : OrderTopology α],
t = TopologicalSpace.generateFrom {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a}
The theorem `OrderTopology.topology_eq_generate_intervals` states that for any type `α`, given a topological space `t` over `α`, a preorder on `α`, and an order topology `self`, the topology `t` can be generated by the collection of open intervals formed by `Set.Ioi a` (left-open right-infinite intervals) and `Set.Iio a` (left-infinite right-open intervals) for some element `a` in `α`. This means the topology `t` can be created by the set of all open intervals that are either of the form `(a, ∞)` or `(-∞, a)`.
More concisely: A topology over a type `α` can be generated by the collection of left-open and right-infinite intervals with respect to a given preorder and order topology.
|
StrictMono.induced_topology_eq_preorder
theorem StrictMono.induced_topology_eq_preorder :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] [t : TopologicalSpace β]
[inst_2 : OrderTopology β] {f : α → β},
StrictMono f → (Set.range f).OrdConnected → TopologicalSpace.induced f t = Preorder.topology α
This theorem states that for any two types `α` and `β` with linear order, if `β` also has a topological space and order topology, and if there is a strictly monotone function `f` from `α` to `β` such that the range of `f` is order-connected, then the topology induced by `f` is equivalent to the preorder topology on `α`. In simpler terms, the topology on `α` that makes `f` continuous is the same as the topology generated by the subbase of open intervals derived from the order on `α`.
More concisely: If `α` and `β` are types with linear orders, `β` has a topological space and order topology, and there exists a strictly monotone function `f` from `α` to `β` with a connected range, then the topology induced by `f` on `α` equals the preorder topology on `α`.
|
mem_nhds_iff_exists_Ioo_subset'
theorem mem_nhds_iff_exists_Ioo_subset' :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α] {a : α} {s : Set α},
(∃ l, l < a) → (∃ u, a < u) → (s ∈ nhds a ↔ ∃ l u, a ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ s)
This theorem states that for a given set `s` and an element `a` of a linear ordered topological space `α`, `s` is a neighborhood of `a` if and only if there exist elements `l` and `u` such that `a` is in the open interval `(l, u)` and this interval is a subset of `s`. This is provided that `a` is not a bottom or top element, meaning there exist elements `l` and `u` in `α` such that `l` is less than `a` and `a` is less than `u`, respectively.
More concisely: A set `s` is a neighborhood of an element `a` in a linear ordered topological space if and only if `a` is an interior point of the open interval `(l, u)` that is a subset of `s`, where `l` and `u` are elements strictly less and greater than `a`, respectively.
|
countable_setOf_covBy_right
theorem countable_setOf_covBy_right :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst : SecondCountableTopology α], {x | ∃ y, x ⋖ y}.Countable
The theorem `countable_setOf_covBy_right` states that for any type `α`, given a topological space, a linear order, an order topology, and a second countable topology, the set of points in `α` that are strictly less than some other points (i.e., the set of points which are isolated on the right) is countable.
More concisely: The set of points in a type `α` that are isolated on the right under an order topology in a second countable topological space is countable.
|
nhds_top_order
theorem nhds_top_order :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : OrderTop α] [inst_3 : OrderTopology α],
nhds ⊤ = ⨅ l, ⨅ (_ : l < ⊤), Filter.principal (Set.Ioi l)
This theorem states that for any type `α` that has a topological space structure, a preorder, a greatest element (`⊤`), and for which the order and the topology are compatible (an order topology), the neighborhood filter at the top element `⊤` is the infimum of the principal filter of the set of elements greater than `l`, for all `l` less than `⊤`. In other words, the neighborhoods of the greatest element in such a space are precisely the collections of sets containing a right-open interval `(l, ∞)` for some `l` less than `⊤`.
More concisely: In a topological preorder space with a greatest element and compatible order topology, the neighborhood filter at the greatest element is the infimum of the principal filters of elements strictly less than it.
|
gt_mem_nhds
theorem gt_mem_nhds :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderTopology α] {a b : α},
a < b → ∀ᶠ (x : α) in nhds a, x < b
The theorem `gt_mem_nhds` states that for any two elements `a` and `b` of a certain type `α`, where `α` is equipped with a topological space structure, a preorder structure, and an order topology, if `a` is strictly less than `b`, then all elements `x` that are sufficiently close to `a` (i.e., within a neighborhood of `a`) are strictly less than `b`. Here, "sufficiently close" is defined in terms of the neighborhood filter `nhds`.
More concisely: For any topological preorder space `(α, ≤, top)` with order topology `top`, if `a ≤ b` does not hold and `x ∈ nhds a`, then `x < b`.
|
tendsto_order
theorem tendsto_order :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderTopology α] {f : β → α}
{a : α} {x : Filter β},
Filter.Tendsto f x (nhds a) ↔ (∀ a' < a, ∀ᶠ (b : β) in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ (b : β) in x, f b < a'
This theorem, `tendsto_order`, establishes a characterization of the limit of a function in terms of order theory. Given a function `f` from type `β` to `α` where `α` has a topology and a preorder structure and the topology is compatible with this preorder, then we say that the function `f` tends towards `a` as per the filter `x` if and only if for all values `a'` less than `a`, eventually (as dictated by the filter `x`), the function `f` mapped to `b` is greater than `a'`, and similarly for all `a'` greater than `a`, eventually, the function `f` mapped to `b` is less than `a'`. Here, "eventually" refers to the filter on `β` which can be thought of as a generalized notion of sequence or condition that becomes true "in the limit".
More concisely: Given a compatible preorder and topology on `α`, a function `f : β → α` tends towards `a` as per filter `x` if and only if for all `a' < a`, eventually `f(b) > a'` for some `b ∈ x`, and for all `a' > a`, eventually `f(b) < a'` for some `b ∈ x`.
|
Mathlib.Topology.Order.Basic._auxLemma.14
theorem Mathlib.Topology.Order.Basic._auxLemma.14 :
∀ {α : Type u_1} {p : αᵒᵈ → Prop}, (∃ a, p a) = ∃ a, p (OrderDual.toDual a)
The `Mathlib.Topology.Order.Basic._auxLemma.14` theorem asserts that for any type `α` and any property `p` that can be applied to the dual of `α`, the existence of an element in the dual of `α` satisfying the property `p` is equivalent to the existence of an element in `α` that, when passed through the `OrderDual.toDual` identity function, satisfies the property `p`.
More concisely: For any type `α` and property `p` on its dual, an element in `α` maps to an element in its dual satisfying `p` if and only if there exists an element in the dual satisfying `p`.
|
SecondCountableTopology.of_separableSpace_orderTopology
theorem SecondCountableTopology.of_separableSpace_orderTopology :
∀ (α : Type u) [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] [inst_4 : TopologicalSpace.SeparableSpace α], SecondCountableTopology α
This theorem states that for any type `α` that has a densely ordered linear order with order topology, if `α` is also a separable space, then it has a second countable topology. The densely ordered assumption is crucial to the theorem and cannot be skipped. A counterexample to this can be seen with the "double arrow space".
More concisely: If `α` is a separable space with a densely ordered linear structure, then `α` has a second countable topology.
|
dense_of_exists_between
theorem dense_of_exists_between :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : Nontrivial α] {s : Set α}, (∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, a < c ∧ c < b) → Dense s
This theorem, `dense_of_exists_between`, states that for any type `α` equipped with a topological space structure, a linear order, an order topology, and is nontrivial, and for any set `s` of elements of this type, if for every pair of elements `a` and `b` from `α` such that `a` is less than `b` there exists an element `c` in the set `s` such that `c` is greater than `a` and less than `b`, then the set `s` is dense in the topological space.
In other words, if we have a topological space with a linear order and an order topology, and any two points in this space can be "sandwiched" by a point from a specific set, then this set is dense in the topological space.
More concisely: If a non-empty subset `S` of a topological space `(α,τ)` with a linear order `≤` such that the order induces the given topology `τ`, and for all `a` and `b` in `α` with `a < b`, there exists `c` in `S` with `a < c < b`, then `S` is dense in `(α,τ)`.
|
le_mem_nhds
theorem le_mem_nhds :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderTopology α] {a b : α},
a < b → ∀ᶠ (x : α) in nhds b, a ≤ x
The theorem `le_mem_nhds` states that for any type `α` equipped with a topological space structure, a preorder structure, and an order topology, and for any two elements `a` and `b` of `α` such that `a` is less than `b`, all elements `x` in a neighborhood of `b` (as defined by the neighborhood filter `nhds b`) are greater than or equal to `a`. Essentially, this theorem asserts that in a topological space compatible with an order, if `a` is less than `b`, then there exists a neighborhood around `b` in which all elements are greater than or equal to `a`.
More concisely: For any topological space `(α, top)` with order `≤` and `a ≤ b` in `α`, every neighborhood `N ∈ nhds(b)` satisfies `x ≥ a` for all `x ∈ N`.
|
Mathlib.Topology.Order.Basic._auxLemma.6
theorem Mathlib.Topology.Order.Basic._auxLemma.6 :
∀ {α : Type u} {β : Type v} {ι : Sort x} {f : α → β} {x : Filter α} {y : ι → Filter β},
Filter.Tendsto f x (⨅ i, y i) = ∀ (i : ι), Filter.Tendsto f x (y i)
This theorem states that for any types `α`, `β` and `ι`, a function `f` from `α` to `β`, a filter `x` on type `α`, and a function `y` from `ι` to filters on `β`, the function `f` tends to the infimum of the filters `y i` (denoted by `(⨅ i, y i)`) if and only if the function `f` tends to each filter `y i` for all `i` in `ι`. In other words, the function `f` has a limit at the infimum of the filters if and only if it has a limit at each of the filters.
More concisely: A function from types `α` to `β` tends to the infimum of a family of filters on `β` indexed by `ι` if and only if it tends to each filter in the family for all indices `i` in `ι`.
|
nhds_bot_order
theorem nhds_bot_order :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : OrderBot α] [inst_3 : OrderTopology α],
nhds ⊥ = ⨅ l, ⨅ (_ : ⊥ < l), Filter.principal (Set.Iio l)
This theorem states that for any type `α` that is equipped with a topology, a preorder relationship, an order with a least element (denoted by `⊥`), and an order topology, the neighborhood filter at the least element `⊥` is equal to the infimum of filters generated by left-infinite right-open intervals `Set.Iio l` for all elements `l` such that `⊥` is less than `l`. In simpler terms, the neighborhoods of the least element `⊥` are the smallest open sets that contain all elements smaller than some `l`, where `l` is every element that is greater than `⊥`.
More concisely: The neighborhood filter of the least element in a topological preorder with a least element is equal to the infimum of filters generated by left-infinite right-open intervals containing elements greater than the least element.
|
nhds_eq_order
theorem nhds_eq_order :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderTopology α] (a : α),
nhds a = (⨅ b ∈ Set.Iio a, Filter.principal (Set.Ioi b)) ⊓ ⨅ b ∈ Set.Ioi a, Filter.principal (Set.Iio b)
The theorem `nhds_eq_order` states that for any type `α`, where `α` is given a topological space structure, a preorder structure, and an order topology, for any element `a` in `α`, the neighborhood filter at `a` is equal to the infimum of the principal filters of the right-open left-infinite interval for every element less than `a` intersected with the infimum of the principal filters of the left-open right-infinite interval for every element greater than `a`. In simpler terms, this theorem describes how the neighborhoods of a point in an ordered topological space can be constructed from intervals that are open to the right and contain all smaller elements, and intervals that are open to the left and contain all larger elements.
More concisely: The neighborhood filter of an element in an ordered topological space is equal to the infimum of the principal filters of right-open, left-infinite intervals containing smaller elements, intersected with the infimum of the principal filters of left-open, right-infinite intervals containing larger elements.
|
countable_of_isolated_left'
theorem countable_of_isolated_left' :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst : SecondCountableTopology α], {x | ∃ y < x, Set.Ioo y x = ∅}.Countable
This theorem states that for any type 'α' which is equipped with a topological space structure, a linear order structure, an order topology, and a second-countable topology, the set of points 'x' which have an isolated point 'y' to their left (i.e., there exists a 'y' such that 'y' is less than 'x' and the open interval between 'y' and 'x' is empty) is countable. In other words, in a second-countable topological space ordered linearly, the quantity of points that have no other points immediately to their left is countable.
More concisely: In a second-countable, linearly ordered topological space, the set of points with an isolated left point is countable.
|
tendsto_of_tendsto_of_tendsto_of_le_of_le
theorem tendsto_of_tendsto_of_tendsto_of_le_of_le :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderTopology α] {f g h : β → α}
{b : Filter β} {a : α},
Filter.Tendsto g b (nhds a) → Filter.Tendsto h b (nhds a) → g ≤ f → f ≤ h → Filter.Tendsto f b (nhds a)
The **Squeeze theorem**, also known as the **sandwich theorem**, asserts the following: Given a topological space with a preorder relation and a set of three functions `f`, `g`, and `h` mapping from a set `β` to the elements of the space, along with a filter `b` on `β` and an element `a` of the space, if `g` and `h` both tend to `a` (that is, their images under `b` converge to `a`), and `f` is bounded from below by `g` and from above by `h` (that is, `g ≤ f ≤ h` holds everywhere), then `f` also tends to `a`. In other words, if `f` is squeezed between `g` and `h`, and both `g` and `h` converge to the same limit, then `f` converges to the same limit as well.
More concisely: If functions `f`, `g`, and `h` map a set to a topological space, `g` and `h` converge to a point `a` in the space, and `g ≤ f ≤ h` holds everywhere, then `f` also converges to `a`.
|
isOpen_lt'
theorem isOpen_lt' :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderTopology α] (a : α),
IsOpen {b | a < b}
This theorem states that for any type `α` which has a topological space structure, a preorder (a binary relation that is reflexive and transitive), and an order topology (a certain topology defined on a totally ordered set), and for any element `a` of this type, the set of elements `b` in `α` such that `a` is less than `b` forms an open set in the given topological space. In mathematical terms, this can be written as: for all `a` in `α`, the set `{b | a < b}` is open in the topological space `α`.
More concisely: For any type `α` endowed with a topological space structure, a preorder, and an order topology, the upward closed balls in the order topology are open sets. (Here, an upward closed ball with center `a` is the set `{b | a < b}`).
|
countable_setOf_covBy_left
theorem countable_setOf_covBy_left :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst : SecondCountableTopology α], {x | ∃ y, y ⋖ x}.Countable
This theorem states that in any second-countable topological space, ordered linearly and with an order topology, the set of points which have at least one other point strictly less than them (i.e., the set of points isolated on the left) is countable. In other words, there are countably many points in such a space where another point can be found that is strictly less than the given point.
More concisely: In a second-countable, linearly ordered topological space, the set of points with strictly lesser neighbors is countable.
|
countable_image_lt_image_Ioi
theorem countable_image_lt_image_Ioi :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] (f : β → α) [inst : SecondCountableTopology α],
{x | ∃ z, f x < z ∧ ∀ (y : β), x < y → z ≤ f y}.Countable
This theorem states that for a function `f` that maps elements from a type `β` to a type `α` (with `α` being a topological space with a second countable topology and a linear order that is also an order topology, and `β` a linear order), the set of points `x` in `β` for which the image of `(x, ∞)` under `f` is always equal to or greater than some value `z` that is greater than `f(x)` is a countable set. In other words, it's the set of points `x` in `β` where `f(x)` is strictly less than some `z`, and for all `y` greater than `x`, `f(y)` is always at least `z`.
More concisely: For a function `f` from a linearly ordered type `β` to a second countable topological space `α` with a linear order that is also an order topology, the set of `x` in `β` such that for all `y > x`, `f(y)` is greater than or equal to `f(x) + z`, for some `z > f(x)`, is countable.
|
Set.PairwiseDisjoint.countable_of_Ioo
theorem Set.PairwiseDisjoint.countable_of_Ioo :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst : SecondCountableTopology α] {y : α → α} {s : Set α},
(s.PairwiseDisjoint fun x => Set.Ioo x (y x)) → (∀ x ∈ s, x < y x) → s.Countable
This theorem states that for a second-countable topological space `α` with linear order and order topology, consider a disjoint family of open intervals `(x, y(x))` for `x` in some set `s` such that `x < y(x)`. Then, this family of intervals is countable. Here, disjoint means that for any two different elements in the set, their corresponding intervals do not overlap. The theorem notes that this conclusion is not an obvious consequence of the space being second-countable because some of these intervals might be empty. However, the theorem assures that only countably many intervals can be empty.
More concisely: A second-countable topological space with a linear order and disjoint family of open intervals of the form (x, y(x)) with x in some set and x < y(x) contains at most countably many empty intervals.
|
nhdsWithin_Ici_basis'
theorem nhdsWithin_Ici_basis' :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α] {a : α},
(∃ u, a < u) → (nhdsWithin a (Set.Ici a)).HasBasis (fun u => a < u) fun u => Set.Ico a u
The theorem `nhdsWithin_Ici_basis'` states that for any type `α` endowed with a topological space structure, a linear order and an order topology, and for any element `a` of that type `α`, given that there exists an element `u` in `α` such that `a` is less than `u`, the filter of the neighborhood within the set comprising of all elements greater than or equal to `a` (denoted by `Set.Ici a`) at the point `a` has a basis indexed by the sets of elements `u` where `u` is greater than `a`, and the basis elements are the sets of all `x` in `α` such that `x` is greater than or equal to `a` and less than `u` (denoted by `Set.Ico a u`). In simpler terms, this theorem provides a characterization of the neighborhoods within right-closed infinite intervals in terms of left-closed right-open intervals.
More concisely: For any type endowed with a topological space structure, a linear order, and an order topology, the filter of neighborhoods at an element `a` with `a < u` for some `u` in the type has a basis consisting of left-closed right-open intervals `Set.Ico a u`.
|
countable_image_gt_image_Ioi
theorem countable_image_gt_image_Ioi :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] (f : β → α) [inst : SecondCountableTopology α],
{x | ∃ z < f x, ∀ (y : β), x < y → f y ≤ z}.Countable
The theorem `countable_image_gt_image_Ioi` states that for any function `f` mapping from a type `β` to a type `α` (where `α` is a second countable topological space under a linear order and an order topology, and `β` is under a linear order), the set of all points `x` in `β` such that there exists a `z` less than `f(x)` and for all `y` in `β` (where `x` is less than `y`), `f(y)` is less than or equal to `z`, is countable. In other words, the set of points `x` for which the image under `f` of `(x, ∞)` is separated below from `f(x)` is countable.
More concisely: The set of elements in a linearly ordered type `β`, such that the image under a function `f` from `β` to a second countable, linearly ordered space `α` admits a lower bound strictly below the image of that element and is less than or equal to the image of every strictly greater element, is countable.
|
exists_Ioc_subset_of_mem_nhds
theorem exists_Ioc_subset_of_mem_nhds :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α] {a : α} {s : Set α},
s ∈ nhds a → (∃ l, l < a) → ∃ l < a, Set.Ioc l a ⊆ s
This theorem states that for any type `α` that has a topological space structure, a linear order and an order topology, and for any element `a` of type `α` and a set `s` of type `α`, if `s` is a neighborhood of `a` and there exists an element `l` that is less than `a`, then there exists an element `l` that is less than `a` such that the left-open right-closed interval from `l` to `a` is a subset of `s`. In other words, given a neighborhood around a point in an ordered topological space and an element less than the point, we can always find a left-open right-closed interval that fits within the neighborhood and whose upper limit is the given point.
More concisely: For any ordered topological space `(α, ≤, τ)` and `a ∈ α` with `s ∈ ν(a)` (the neighborhood filter of `a`), if there exists `l < a` such that `(l, a] ⊆ s`, then there exists such `l` with `(l, a] ∈ τ`.
|
Mathlib.Topology.Order.Basic._auxLemma.7
theorem Mathlib.Topology.Order.Basic._auxLemma.7 :
∀ {α : Type u} {β : Type v} {f : α → β} {l : Filter α} {s : Set β},
Filter.Tendsto f l (Filter.principal s) = ∀ᶠ (a : α) in l, f a ∈ s
The theorem `Mathlib.Topology.Order.Basic._auxLemma.7` states that for any types `α` and `β`, a function `f` from `α` to `β`, a filter `l` on `α`, and a set `s` of `β`, the function `f` tends to the principal filter of `s` under the filter `l` if and only if almost every element `a` in the filter `l` satisfies that `f(a)` is an element of `s`. In other words, the function `f` maps almost all elements in the neighborhood described by the filter `l` into the set `s`. Here, "almost every element" refers to the concept of "eventually", meaning that apart from possibly a finite number of exceptions, all elements satisfy the condition.
More concisely: A function from a type to another tends to the principal filter of a set under a given filter if and only if almost all elements in the filter map to elements in the set.
|
countable_image_gt_image_Iio
theorem countable_image_gt_image_Iio :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] (f : β → α) [inst : SecondCountableTopology α],
{x | ∃ z < f x, ∀ y < x, f y ≤ z}.Countable
The theorem `countable_image_gt_image_Iio` states that for any function `f` mapping elements from an ordered type `β` to a topological space `α` (which is also ordered and obeys the order topology), if `α` has second countable topology, then the set of all `x` in `β` satisfying the property that there exists some `z` less than `f(x)` such that for all `y` less than `x`, `f(y)` is less than or equal to `z` is countable. This essentially means that the set of all `x` where the image of the interval `(-∞, x)` under `f` is strictly less than `f(x)` is countable.
More concisely: If `f: β -> α` is a function from an ordered type `β` to a second countable, ordered topological space `α`, then the set of `x` in `β` such that `f(x)` is strictly larger than the supremum of `f` over all `y` less than `x` is countable.
|
lt_mem_nhds
theorem lt_mem_nhds :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderTopology α] {a b : α},
a < b → ∀ᶠ (x : α) in nhds b, a < x
This theorem states that for any types `α`, which is a topological space with a preorder and order topology, and any two elements `a` and `b` of type `α`, if `a` is less than `b`, then there exists a neighborhood around `b` such that every element `x` in this neighborhood satisfies the condition that `a` is less than `x`. This is a result in order topology, which connects the concepts of order and topology in a consistent way.
More concisely: For any topological space with a preorder endowed with order topology, if `a` is less than `b`, then there exists a neighborhood of `b` where `a` is less than every element.
|
dense_iff_exists_between
theorem dense_iff_exists_between :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] [inst_4 : Nontrivial α] {s : Set α},
Dense s ↔ ∀ (a b : α), a < b → ∃ c ∈ s, a < c ∧ c < b
This theorem states that for a set in a nontrivial densely linearly ordered type, the set is considered dense in the context of the topology if and only if for any two elements `a` and `b` with `a < b`, there exists an element `c` in the set such that `a < c < b`. That is, between any two distinct elements in the ordered type, there exists an element from the set in between. The theorem also mentions that each direction of this equivalence depends on fewer typeclass assumptions. Here, the topological space, linear order, order topology, densely ordered, and nontriviality are properties of the type of the elements in the set.
More concisely: For a dense subset of a nontrivial linearly ordered type, for all `a < b` in the type, there exists `c` in the subset with `a < c < b`.
|
nhds_top_basis
theorem nhds_top_basis :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTop α] [inst_3 : OrderTopology α]
[inst_4 : Nontrivial α], (nhds ⊤).HasBasis (fun a => a < ⊤) fun a => Set.Ioi a
This theorem states that for any type `α` that is equipped with a topology, a linear order, a top element, an order topology, and is nontrivial, the neighborhood filter at the top element `⊤` has a basis consisting of the sets that are open intervals `(a, ∞)` where `a` is any element less than `⊤`. In other words, every neighbourhood of `⊤` contains such an interval for some `a`, and given `a < ⊤`, there is such a neighborhood.
More concisely: For any nontrivial type `α` with a topology, a linear order, and a top element `⊤`, the neighborhood filter at `⊤` has a basis consisting of open intervals `(a, ∞)` for all `a` less than `⊤`.
|
mem_nhds_iff_exists_Ioo_subset
theorem mem_nhds_iff_exists_Ioo_subset :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : NoMaxOrder α] [inst_4 : NoMinOrder α] {a : α} {s : Set α},
s ∈ nhds a ↔ ∃ l u, a ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ s
This theorem states that a set is a neighborhood of a point 'a' in a topological space if and only if there exist two points 'l' and 'u' such that 'a' lies in the open interval '(l, u)' and this open interval is a subset of the set. The theorem applies in a context where we have a topological space, a linear order, an order topology, and additionally there is no greatest or least element overall. This result links the concept of neighborhoods in topology with the more concrete notion of open intervals in an ordered set.
More concisely: A set is a neighborhood of a point in a topological space without greatest or least elements if and only if the point lies in an open interval contained in the set and the interval is a subset of the set.
|
nhds_bot_basis
theorem nhds_bot_basis :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderBot α] [inst_3 : OrderTopology α]
[inst_4 : Nontrivial α], (nhds ⊥).HasBasis (fun a => ⊥ < a) fun a => Set.Iio a
This theorem states that, for any type `α` which has a topological space, linear ordering, a least element (`OrderBot`), an order topology and is nontrivial, the neighborhood filter at the least element (`nhds ⊥`) has a basis given by sets of the form `Set.Iio a`, where `a` is any element greater than the least element. In other words, the basis sets for the neighborhood filter at the bottom element are all left-infinite, right-open intervals that start from the least element and end just before `a`, for all `a` in `α` that are greater than the least element.
More concisely: For any nontrivial type `α` with a topological space structure, a linear ordering, a least element, and an order topology, the basis for the neighborhood filter at the least element is given by sets of the form `(a -- ε)`, where `a` is any element strictly greater than the least element.
|
tendsto_of_tendsto_of_tendsto_of_le_of_le'
theorem tendsto_of_tendsto_of_tendsto_of_le_of_le' :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderTopology α] {f g h : β → α}
{b : Filter β} {a : α},
Filter.Tendsto g b (nhds a) →
Filter.Tendsto h b (nhds a) →
(∀ᶠ (b : β) in b, g b ≤ f b) → (∀ᶠ (b : β) in b, f b ≤ h b) → Filter.Tendsto f b (nhds a)
This is the **Squeeze Theorem**, also known as the **Sandwich Theorem**, in the context of filters. Given a topological space `α` with a preorder and an order topology, and three functions `f`, `g`, and `h` from `β` to `α`, and a filter `b` on `β` and a point `a` in `α`, if `g` and `h` both tend to `a` as defined by the filter `b`, and if `g(b)` is eventually less than or equal to `f(b)` and `f(b)` is eventually less than or equal to `h(b)` under the filter `b`, then `f` also tends to `a` under the filter `b`. In simpler terms, if `f` is squeezed between `g` and `h` for values in `b` and both `g` and `h` approach the same limit `a`, then `f` also approaches `a`.
More concisely: If functions `f`, `g`, and `h` satisfy `g(x) ≤ f(x) ≤ h(x)` for all `x` in a filter `b` and `g` and `h` both tend to a limit `a` in a topological space with order topology, then `f` also tends to `a` in the filter `b`.
|
ge_mem_nhds
theorem ge_mem_nhds :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderTopology α] {a b : α},
a < b → ∀ᶠ (x : α) in nhds a, x ≤ b
This theorem, `ge_mem_nhds`, states that for any topological space `α` supplied with a preorder and an order topology, and for any two elements `a` and `b` in `α` such that `a` is less than `b`, there exists a neighborhood of `a` in which all elements `x` are less than or equal to `b`. In less formal terms, it says that if `a` is less than `b`, there will always be a set of points close to `a` that are all less than or equal to `b`. Note that `∀ᶠ (x : α) in nhds a, x ≤ b` is a notation in Lean 4 to denote that the set `{x : α | x ≤ b}` is in the neighborhood filter of `a`.
More concisely: For any topological space equipped with a preorder and order topology, if `a` is less than `b`, then there exists a neighborhood of `a` containing only elements less than or equal to `b`.
|
exists_Ico_subset_of_mem_nhds
theorem exists_Ico_subset_of_mem_nhds :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α] {a : α} {s : Set α},
s ∈ nhds a → (∃ u, a < u) → ∃ u, a < u ∧ Set.Ico a u ⊆ s
This theorem states that for any type `α` equipped with both a topological space structure and a linear order structure that is consistent with the topology (i.e. it is an order topology), given any element `a` of type `α` and a set `s` of type `α`, if `s` is a neighborhood of `a` and there exists some element `u` in `α` such that `a` is less than `u`, then there exists another element `u` such that `a` is less than this `u` and the left-closed right-open interval from `a` to `u` is a subset of `s`. Basically, it guarantees the existence of an interval around `a` which is contained inside a given neighborhood whenever `a` is not a maximal element.
More concisely: Given a topological space `(α, τ)` with a compatible linear order `≤`, if `a ∈ α`, `s ⊆ α` is a neighborhood of `a`, and there exists `u ∈ α` with `a < u`, then there exists `u' < u` such that `[a, u) ⊆ s`.
|
countable_image_lt_image_Iio
theorem countable_image_lt_image_Iio :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] (f : β → α) [inst : SecondCountableTopology α],
{x | ∃ z, f x < z ∧ ∀ y < x, z ≤ f y}.Countable
The theorem `countable_image_lt_image_Iio` states that for a function `f` mapping from any linearly ordered type `β` to a second countable topological space `α`, the set of points `x` in `β` such that there exists a `z` where `f(x)` is less than `z` and for all `y` less than `x`, `f(y)` is less or equal to `z` is countable. Here, the conditions on `f(x)` and `f(y)` effectively mean that the image of `(-∞, x)` under `f` is separated above from `f(x)`.
More concisely: The set of elements in a linearly ordered type mapping to a second countable space, such that their image is strictly less than some point and their predecessors map below it, is countable.
|
isOpen_gt'
theorem isOpen_gt' :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderTopology α] (a : α),
IsOpen {b | b < a}
The theorem `isOpen_gt'` states that for any type `α` that has a topological space structure, a preorder (a binary relation that is reflexive and transitive), and an order topology (a topology induced by a total order), and for any element `a` of type `α`, the set of all elements `b` such that `b` is less than `a` is an open set in the given topological space. This is a statement about order topologies and clarifies their properties with respect to open sets.
More concisely: For any type `α` with a topological space structure, a preorder, and an order topology, the subset of elements less than any given element `a` is an open set.
|