Ioi_mem_nhdsSet_Icc
theorem Ioi_mem_nhdsSet_Icc :
∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderClosedTopology α] {a b c : α},
a < b → Set.Ioi a ∈ nhdsSet (Set.Icc b c)
This theorem states that for any three elements `a`, `b`, and `c` of a type `α` endowed with a linear order and a topological space structure in which the order is closed, if `a` is less than `b`, then the set of elements greater than `a` (`Set.Ioi a`) is a neighborhood of the closed interval from `b` to `c` (`Set.Icc b c`). In other words, `Set.Ioi a` is in the filter of neighborhoods of the set `Set.Icc b c`.
More concisely: For any type `α` with a linear order and a topology where order intervals are closed, if `a < b` then the set of elements greater than `a` is a neighborhood of the closed interval `[b, c]`.
|
Iic_mem_nhdsSet_Icc
theorem Iic_mem_nhdsSet_Icc :
∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderClosedTopology α] {a b c : α},
b < c → Set.Iic c ∈ nhdsSet (Set.Icc a b)
The theorem `Iic_mem_nhdsSet_Icc` states that for any given type `α` which is a linearly ordered topological space with the orderings closed, and any three elements `a`, `b`, `c` of this type, if `b` is less than `c`, then the left-infinite right-closed interval `Set.Iic c` (consisting of all elements less than or equal to `c`) is a member of the filter of neighborhoods (`nhdsSet`) of the closed interval `Set.Icc a b` (consisting of all elements `x` such that `a ≤ x ≤ b`). In practical terms, this means that we can always find a left-infinite right-closed interval whose end point is greater than the upper bound of our given closed interval, and this interval will be a neighborhood of our original closed interval in the given topological space.
More concisely: For any linearly ordered topological space `α` with closed orderings, if `b` is less than `c` in `α`, then `Set.Iic c ∈ nhdsSet (Set.Icc a b)`.
|
Ici_mem_nhdsSet_Icc
theorem Ici_mem_nhdsSet_Icc :
∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderClosedTopology α] {a b c : α},
a < b → Set.Ici a ∈ nhdsSet (Set.Icc b c)
This theorem states that for any type `α` that has a linear order, a topological space structure, and an order-closed topology, and for any three elements `a`, `b`, and `c` of this type, if `a` is less than `b`, then the left-closed right-infinite interval starting from `a` is an element of the filter of neighborhoods of the left-closed right-closed interval from `b` to `c`. In other words, the set of all elements greater than or equal to `a` is in the vicinity of the set of all elements between `b` and `c` (inclusive) in the given topological structure.
More concisely: For any type `α` with a linear order, topology, and order-closed topology, if `a < b <= c`, then the filter of neighborhoods of the interval [`b, c`] contains the set `{x : α | x >= a}`.
|
Iio_mem_nhdsSet_Ico
theorem Iio_mem_nhdsSet_Ico :
∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderClosedTopology α] {a b c : α},
b ≤ c → Set.Iio c ∈ nhdsSet (Set.Ico a b)
This theorem states that for any given type `α` which has a linear order, a topological space structure, and an order closed topology, and for any three elements `a`, `b`, and `c` of this type where `b` is less than or equal to `c`, the left-infinite right-open interval ending at `c` is an element of the filter of neighborhoods of the left-closed right-open interval from `a` to `b`. In other words, the set of all elements less than `c` is a neighborhood of the interval `[a, b)` in the given topological space.
More concisely: For any type `α` with a linear order, topology, and order-closed topology, if `a < b <= c` are elements of `α`, then the set of elements strictly less than `c` is a neighborhood of the interval `[a, b)` in the given topology.
|
Ioi_mem_nhdsSet_Ioc
theorem Ioi_mem_nhdsSet_Ioc :
∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderClosedTopology α] {a b c : α},
a ≤ b → Set.Ioi a ∈ nhdsSet (Set.Ioc b c)
This theorem states that for any types `α` which is a linear order and a topological space with order-closed topology, and any three elements `a`, `b` and `c` of `α`, if `a` is less than or equal to `b`, then the left-open right-infinite interval from `a` (`Set.Ioi a`) is a neighborhood within the filter of neighborhoods of the left-open right-closed interval from `b` to `c` (`Set.Ioc b c`). In other words, the open interval greater than `a` is in the neighborhood of the set of points that are strictly greater than `b` and less than or equal to `c` in this topological space.
More concisely: For any linear order and topological space `α` with order-closed topology, if `a ≤ b` in `α`, then `Set.Ioi a ⊆ Set.Ioc b c` in the filter of neighborhoods of `α`.
|
Iio_mem_nhdsSet_Icc
theorem Iio_mem_nhdsSet_Icc :
∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderClosedTopology α] {a b c : α},
b < c → Set.Iio c ∈ nhdsSet (Set.Icc a b)
This theorem states that for any type `α` that is equipped with a linear order, a topological space structure, and an order-closed topology, and for any three elements `a`, `b`, and `c` of this type where `b < c`, then the left-infinite right-open interval ending at `c`, denoted `Set.Iio c`, is a neighborhood of the closed interval between `a` and `b`, denoted `Set.Icc a b`. In other words, there are open sets in the topology on `α` which contain the closed interval from `a` to `b` and are contained in the half-open interval from `-∞` to `c`.
More concisely: For any type `α` with a linear order, topology, and order-closed topology, the left-infinite right-open interval `Set.Iio c` is a neighborhood of the closed interval `Set.Icc a b` for any `a < b` in `α`.
|
Ioi_mem_nhdsSet_Ici
theorem Ioi_mem_nhdsSet_Ici :
∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderClosedTopology α] {a b : α},
a < b → Set.Ioi a ∈ nhdsSet (Set.Ici b)
The theorem `Ioi_mem_nhdsSet_Ici` states that for any type `α` that has a linear order, a topological space and an order-closed topology, and for any two elements `a` and `b` of this type, if `a` is less than `b`, then the left-open right-infinite interval starting at `a` (`a < x`) is in the filter of neighborhoods of the left-closed right-infinite interval starting at `b` (`b ≤ x`). In other words, if `b` is a limit point of some set, the interval `(a, ∞)` is a neighborhood of `b` in the topological space.
More concisely: For any type with a linear order and an order-closed topology, if `a` is strictly less than `b`, then the left-open right-infinite interval `(a, ∞)` is in the filter of neighborhoods of the left-closed right-infinite interval `[b, ∞)` in the topological space.
|
Iio_mem_nhdsSet_Iic
theorem Iio_mem_nhdsSet_Iic :
∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderClosedTopology α] {a b : α},
a < b → Set.Iio b ∈ nhdsSet (Set.Iic a)
The theorem `Iio_mem_nhdsSet_Iic` states that for any given types `α` that have a linear order and a topological space structure with an order-closed topology, and for any two elements `a` and `b` of this type `α`, if `a` is less than `b`, then the left-infinite right-open interval less than `b` (`Set.Iio b`) is within the filter of neighborhoods of the left-infinite right-closed interval less than or equal to `a` (`nhdsSet (Set.Iic a)`). In other words, the set of all elements less than `b` is in the neighborhood of the set of all elements less or equal to `a` in the given topological space, if `a < b`.
More concisely: For any type `α` with a linear order and an order-closed topology, if `a < b` in `α`, then `Set.Iio b ∈ nhdsSet (Set.Iic a)`.
|