comap_coe_nhdsWithin_Iio_of_Ioo_subset
theorem comap_coe_nhdsWithin_Iio_of_Ioo_subset :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] {b : α} {s : Set α},
s ⊆ Set.Iio b →
(s.Nonempty → ∃ a < b, Set.Ioo a b ⊆ s) → Filter.comap Subtype.val (nhdsWithin b (Set.Iio b)) = Filter.atTop
This theorem states that for any type `α` equipped with a topological space structure, a linear order, an order topology, and a densely ordered structure, given any element `b` of type `α` and a subset `s` of type `α`, if `s` is a subset of the left-infinite right-open interval ending at `b` and if `s` is not empty, then there exists an element `a` less than `b` such that the left-open right-open interval between `a` and `b` is a subset of `s`. Under these conditions, the filter obtained by mapping elements of the neighborhood within the set `s` at `b` to their underlying elements in the base type (using the `comap` function and the value function for subtypes `Subtype.val`), is equal to the filter representing the limit `→ ∞` on an ordered set (given by `Filter.atTop`).
More concisely: For any densely ordered and topological space `(α, ≤, top)`, given a non-empty subset `s` of the left-infinite right-open interval `(a, b]` with `a < b`, there exists an element `a' < b` such that the filter of neighborhoods of `b` in `s` equals the filter of elements approaching `b` in the order topology.
|
frontier_Ici
theorem frontier_Ici :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] [inst_4 : NoMinOrder α] {a : α}, frontier (Set.Ici a) = {a}
The theorem `frontier_Ici` states that for any type `α` that has a topology, is linearly ordered, has an order topology, is densely ordered, and has no minimum element, the frontier of the left-closed right-infinite interval starting at any point `a` is the singleton set containing only 'a'. In other words, the only point that lies between the closure and the interior of this interval is its left endpoint 'a'.
More concisely: For any linearly ordered type with topology, dense order, no minimum element, the frontier of the left-closed right-infinite interval equals its left endpoint.
|
Dense.exists_countable_dense_subset_no_bot_top
theorem Dense.exists_countable_dense_subset_no_bot_top :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] [inst_4 : Nontrivial α] {s : Set α} [inst_5 : TopologicalSpace.SeparableSpace ↑s],
Dense s → ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∉ t) ∧ ∀ (x : α), IsTop x → x ∉ t
This theorem states that given a dense set `s` in a nontrivial densely ordered linear space `α` with a topology that is order-related, if `s` is a separable space (for example, if `α` has a topology which can be covered by countably many open sets), then there exists a countable dense subset `t` of `s` such that `t` does not contain either the greatest or least elements of `α`. In other words, in the context of a topological space that is separable and densely ordered, we can always find a countable dense subset that does not include the extreme elements (lowest and highest) of the space.
More concisely: In a separable, densely ordered, and nontrivial linear space with an order-related topology, there exists a countable dense subset without the greatest or least elements.
|
closure_Iio
theorem closure_Iio :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] (a : α) [inst_4 : NoMinOrder α], closure (Set.Iio a) = Set.Iic a
The theorem `closure_Iio` states that for any type `α` that is equipped with a topological space structure, linear order, order topology, and the property of being densely ordered and without a minimum element, the closure of the left-infinite right-open interval `(-∞, a)` is the left-infinite right-closed interval `(-∞, a]`. In mathematical terms, this means that when you take the closure of the set of all elements less than `a`, you get the set of all elements less than or equal to `a`. This highlights that the boundary value `a` is included in the closure of the open interval.
More concisely: For a densely ordered and without-minimum-element type `α` with topology, the closure of the left-infinite right-open interval `(-∞, a)` equals the left-infinite right-closed interval `(-∞, a]`.
|
closure_Ioi
theorem closure_Ioi :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] (a : α) [inst_4 : NoMaxOrder α], closure (Set.Ioi a) = Set.Ici a
The theorem `closure_Ioi` states that for any type `α` that is a topological space, a linear order, has order topology, is densely ordered, and has no maximum element, the closure of the interval `(a, +∞)` is the closed interval `[a, +∞)`. In mathematical terms, it means that the smallest closed set containing all elements greater than `a` is the set of all elements greater than or equal to `a`. This is valid in a context where the order is compatible with the topology (i.e., it has an order topology) and every two elements have another one strictly between them (i.e., the order is densely ordered), and there is no maximum element in the set.
More concisely: In a densely ordered, topological space without a maximum element and with an order topology, the closure of the open interval (a, +∞) equals the closed interval [a, +∞).
|
closure_Ioc
theorem closure_Ioc :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] {a b : α}, a ≠ b → closure (Set.Ioc a b) = Set.Icc a b
The theorem `closure_Ioc` states that for any type `α` that is a topological space, has a linear order, an order topology, and is densely ordered, and for any two distinct elements `a` and `b` of `α`, the closure of the half-open interval `(a, b]` is the closed interval `[a, b]`. Here, the closure of a set is defined as the smallest closed set containing that set, the half-open interval `(a, b]` includes all elements that are greater than `a` and less than or equal to `b`, and the closed interval `[a, b]` includes all elements that are greater than or equal to `a` and less than or equal to `b`.
More concisely: For any densely ordered topological space `α` with order topology, the closure of the half-open interval `(a, b]` equals the closed interval `[a, b]` for all distinct elements `a` and `b` in `α`.
|
frontier_Iic
theorem frontier_Iic :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] [inst_4 : NoMaxOrder α] {a : α}, frontier (Set.Iic a) = {a}
The theorem `frontier_Iic` states that for any type `α` that is a topological space, has a linear order, is densely ordered, and has no maximum element, the frontier (the set of points between the closure and interior) of the set of all elements less than or equal to a given element `a` is simply the set containing the element `a`. In other words, for any such `α` and `a`, the only point that lies between the closure and interior of the set of all elements less than or equal to `a` is `a` itself. This is in the context of topology, where the frontier of a set is defined as the points which are neither in the interior nor the exterior of the set.
More concisely: For any topological space with a dense linear order and no maximum element, the frontier of the set of elements less than or equal to an element is equal to that element itself.
|
comap_coe_Ioo_nhdsWithin_Ioi
theorem comap_coe_Ioo_nhdsWithin_Ioi :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] (a b : α), Filter.comap Subtype.val (nhdsWithin a (Set.Ioi a)) = Filter.atBot
This theorem states that for any types `α` which is a topological space, a linear order, an order topology, and is densely ordered, and for any two elements `a` and `b` of type `α`, the filter representing the limit approaching negative infinity (`Filter.atBot`) for an open interval `Ioo a b` is equivalent to the filter representing values in the neighborhood of `a` that are greater than `a` (`nhdsWithin a (Set.Ioi a)`), with the mapping function being `Subtype.val` which extracts the underlying element of the subtype. In essence, this theorem is connecting the behavior in the limit of negative infinity in the open interval with the neighborhood of the left endpoint in the ambient order.
More concisely: For any densely ordered type `α` that is a topological space and has an order topology, the filter of elements approaching negative infinity in the open interval `Ioo a b` is equal to the filter of neighborhood elements greater than `a`.
|
closure_Ico
theorem closure_Ico :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] {a b : α}, a ≠ b → closure (Set.Ico a b) = Set.Icc a b
The theorem `closure_Ico` states that for any type `α` that is a topological space, linearly ordered, has an order topology, and is densely ordered, the closure of the left-closed right-open interval `[a, b)` is the left-closed right-closed interval `[a, b]`. This means that if you take the smallest closed set that contains all elements from `a` to `b` not including `b` itself (this is the closure of `[a, b)`), you will end up with the set of all elements from `a` to `b` including `b` (`[a, b]`). This is true given that `a` is not equal to `b`.
More concisely: For a linearly ordered topological space `α` that is densely ordered and has an order topology, the closure of the left-closed right-open interval `[a, b)` equals the left-closed right-closed interval `[a, b]` when `a < b`.
|
map_coe_Ioi_atBot
theorem map_coe_Ioi_atBot :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] (a : α), Filter.map Subtype.val Filter.atBot = nhdsWithin a (Set.Ioi a)
This theorem, `map_coe_Ioi_atBot`, states that for any type `α` that has a topological space structure, a linear order, order topology, and is densely ordered, for any element `a` of `α`, the filter obtained by mapping the `atBot` filter (representing the concept of going to negative infinity) of subtypes of `α` via the function `Subtype.val` (which extracts the element from the subtype) is equal to the neighborhood within the open interval `(a, +∞)` of `a`. In simpler terms, it states that mapping the "going to negative infinity" concept from subtypes to the actual elements results in the concept of "limiting towards `a` from values greater than `a`".
More concisely: For any densely ordered topological space `(α, ≤, τ)` with a topology `τ` induced by the order, the map of the `atBot` filter of subtypes to elements via `Subtype.val` equals the filter of neighborhoods of `a` in the open interval `(a, ∞)`.
|
closure_Iio'
theorem closure_Iio' :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] {a : α}, (Set.Iio a).Nonempty → closure (Set.Iio a) = Set.Iic a
This theorem states that for any type `α` which has structure of a topological space, a linear order, an order topology, and is densely ordered, for any element `a` of `α`, if the set of all elements less than `a` (denoted as `(-∞, a)` in interval notation) is not empty, then the topological closure of this set (the smallest closed set that contains this set) is the set of all elements less than or equal to `a` (denoted as `(-∞, a]` in interval notation) - unless `a` is a bottom element of the order.
More concisely: For any densely ordered topological space `α` with order topology, if an element `a` has a non-empty set of elements strictly less than it, then the topological closure of this set equals the set of all elements less than or equal to `a`, except when `a` is the bottom element.
|
interior_Ici'
theorem interior_Ici' :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] {a : α}, (Set.Iio a).Nonempty → interior (Set.Ici a) = Set.Ioi a
This theorem states that for any type `α` that has a topological space structure, a linear order, an order topology, and is densely ordered, and for any element `a` of `α`, if the set of all elements less than `a` (denoted `Set.Iio a`) is nonempty, then the interior (i.e., the largest open subset) of the set of all elements greater than or equal to `a` (denoted `Set.Ici a`) is exactly the set of all elements strictly greater than `a` (denoted `Set.Ioi a`). In mathematical terms, if `α` is a densely ordered topological space and there exists an element less than `a`, then the interior of the closed interval [a, ∞) is the open interval (a, ∞).
More concisely: In a densely ordered topological space α, the interior of the closed interval [a, ∞) equals the open interval (a, ∞) if and only if α has an element less than a.
|
exists_countable_dense_no_bot_top
theorem exists_countable_dense_no_bot_top :
∀ (α : Type u_1) [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] [inst_4 : TopologicalSpace.SeparableSpace α] [inst_5 : Nontrivial α],
∃ s, s.Countable ∧ Dense s ∧ (∀ (x : α), IsBot x → x ∉ s) ∧ ∀ (x : α), IsTop x → x ∉ s
The theorem `exists_countable_dense_no_bot_top` states that for any given nontrivial separable dense linear order `α`, there exists a countable dense set `s` of `α` which does not contain either the bottom or the top elements of `α`. Specifically, for every `x` in `α`, if `x` is a bottom element, then `x` is not in `s`, and if `x` is a top element, then `x` is not in `s` too. This theorem is about the existence of such a set `s`, and it's applicable in the context of topological spaces, linear orders, order topology, densely ordered sets, separable spaces, and nontrivial orders.
More concisely: For any nontrivial separable dense linear order without a bottom or top element, there exists a countable dense subset that does not contain the bottom or top element.
|
interior_Ici
theorem interior_Ici :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] [inst_4 : NoMinOrder α] {a : α}, interior (Set.Ici a) = Set.Ioi a
The theorem `interior_Ici` states that for any type `α`, given that `α` is equipped with a topological space structure, a linear order, an order topology, is densely ordered, and has no minimum element, then for any element `a` of type `α`, the interior of the set of all elements greater than or equal to `a` (`Set.Ici a`) is equal to the set of all elements strictly greater than `a` (`Set.Ioi a`). Loosely, this means that when you consider the "interior" (the largest open subset) of the left-closed right-infinite interval, you get the left-open right-infinite interval.
More concisely: For a densely ordered topological space without a minimum element `α`, the interior of the set `{x : α | x ≥ a}` is equal to the set `{x : α | x > a}`.
|
interior_Icc
theorem interior_Icc :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] [inst_4 : NoMinOrder α] [inst_5 : NoMaxOrder α] {a b : α},
interior (Set.Icc a b) = Set.Ioo a b
The theorem `interior_Icc` states that for any type `α` that is a topological space, linearly ordered, has an order topology, is densely ordered, and has no minimum or maximum order, the interior of a left-closed right-closed interval (denoted as `Set.Icc a b`) is equal to a left-open right-open interval (denoted as `Set.Ioo a b`). In simpler terms, if we consider the set of all elements that lie in the interval including end points `a` and `b`, then the largest open subset of this set is the set of all elements that lie strictly between `a` and `b`, not including `a` and `b`.
More concisely: For a linearly ordered, topological space `α` without minimum or maximum, having the order topology and density property, the interior of an interval `[a, b]` equals the open interval `(a, b)`.
|
interior_Iic
theorem interior_Iic :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] [inst_4 : NoMaxOrder α] {a : α}, interior (Set.Iic a) = Set.Iio a
The theorem `interior_Iic` states that for any type `α` that has a topological space structure, a linear order structure, an order topology structure, a densely ordered structure, and a NoMaxOrder structure, the interior of the left-infinite right-closed interval up to any point `a` is equal to the left-infinite right-open interval up to `a`. In mathematical terms, this translates to saying that the interior of the half-closed interval `(-∞, a]` is the open interval `(-∞, a)`. This holds in a linearly ordered topological space where every two elements have another element strictly between them and no element is the largest.
More concisely: In a densely ordered, linearly topological space without a maximum element, the interior of the left-infinite right-closed interval equal to the left-infinite right-open interval.
|
comap_coe_Ioo_nhdsWithin_Iio
theorem comap_coe_Ioo_nhdsWithin_Iio :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] (a b : α), Filter.comap Subtype.val (nhdsWithin b (Set.Iio b)) = Filter.atTop
This theorem states that for any two real numbers `a` and `b`, and given that the set of real numbers has a topological space structure, a linear order, order topology, and is densely ordered, the topological filter representing the limit towards infinity (`Filter.atTop`) for an open interval between `a` and `b` (`Ioo a b`) is equivalent to the filter formed by taking the intersection of the left-infinite right-open interval less than `b` (`Set.Iio b`) and a neighborhood of `b` (`nhdsWithin b`), all considered in the ambient order. In essence, it's describing how approaching infinity within an open interval is the same as considering neighborhoods approaching the right endpoint from the left in the real number line.
More concisely: The topological filter of the limit towards infinity in an open interval [a, b] equals the intersection of the left-infinite right-open interval (< b) and a neighborhood of b.
|
closure_Ioo
theorem closure_Ioo :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] {a b : α}, a ≠ b → closure (Set.Ioo a b) = Set.Icc a b
The theorem `closure_Ioo` states that for any type `α` that has a topology, a linear order, an order topology, and is densely ordered, and for any two distinct elements `a` and `b` of this type, the closure of the open interval `(a, b)` is equal to the closed interval `[a, b]`. In mathematical terms, this means that the smallest closed set that contains all the elements `x` such that `a < x < b` is the set of all elements `x` such that `a ≤ x ≤ b`. This theorem is a formalization of a well-known result in real analysis.
More concisely: For any densely ordered type `α` with a topology and order topology, the closure of the open interval `(a, b)` equals the closed interval `[a, b]` for all distinct `a` and `b` in `α`.
|
closure_Ioi'
theorem closure_Ioi' :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] {a : α}, (Set.Ioi a).Nonempty → closure (Set.Ioi a) = Set.Ici a
This theorem states that the closure of the interval `(a, +∞)` is equivalent to the closed interval `[a, +∞)`, unless `a` is a top element. The closure of a set in topology is the smallest closed set that contains the set. Here, the set is an interval of all real numbers greater than `a`. This is true given that the interval `(a, +∞)` is not empty, and under the conditions that we have a topological space, a linear order, an order topology, and a densely ordered set. A densely ordered set is one where between any two distinct elements there's always another one. In essence, no matter how close two elements in the set are, there's always another element in between.
More concisely: The closure of the open interval (a, +∞) in a densely ordered topological space equals the closed interval [a, +∞) if and only if a is not the top element.
|