Ioo_mem_nhdsWithin_Iio'
theorem Ioo_mem_nhdsWithin_Iio' :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : ClosedIicTopology α] {a b : α},
a < b → Set.Ioo a b ∈ nhdsWithin b (Set.Iio b)
This theorem states that for any given type `α` that is a topological space and a linear order with a topology closed at `(-∞, c]`, and for any two elements `a` and `b` of this type such that `a` is less than `b`, the open interval from `a` to `b` (denoted `Set.Ioo a b`) is an element of the "neighborhood within" filter at `b` with respect to the left-infinite right-open interval up to `b` (denoted `nhdsWithin b (Set.Iio b)`). In other words, the open interval `(a, b)` is in the filter generated by intersecting the neighbourhood of `b` and the set of all elements less than `b`.
More concisely: For any topological space and linear order `α` with `α` closed at `(-∞, c]`, and for all `a < b` in `α`, the open interval `(a, b)` is in the neighborhood filter at `b` with respect to the left-infinite right-open interval up to `b`.
|
le_of_tendsto'
theorem le_of_tendsto' :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : ClosedIicTopology α]
{f : β → α} {a b : α} {x : Filter β} [inst_3 : x.NeBot],
Filter.Tendsto f x (nhds a) → (∀ (c : β), f c ≤ b) → a ≤ b
The theorem `le_of_tendsto'` asserts that, for any given types `α` and `β`, where `α` is a topological space with a pre-order relation and a closed interval (`-∞, c]`) topology, and `f` is a function mapping elements of `β` to `α`, if the function `f` tends to a value `a` (i.e., as elements from the filter `x` get closer to `a`, the images under `f` get closer to `a`), and if for every `c` in `β`, `f(c)` is less than or equal to `b`, then `a` is less than or equal to `b`. Here, the filter `x` is assumed to not be the "bottom" filter, a filter that contains no sets.
More concisely: If a function from a pre-ordered topological space to another space, with the property that for every point in the domain and every accumulation point of the domain, the image under the function converges to a limit, and every point in the codomain is less than or equal to the limit for all points in the domain, then the limit is less than or equal to every point in the codomain.
|
isClosed_Ici
theorem isClosed_Ici :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : ClosedIciTopology α] {a : α},
IsClosed (Set.Ici a)
The theorem `isClosed_Ici` states that for any type `α`, given a topology `TopologicalSpace α`, a total order `Preorder α`, and a topology `ClosedIciTopology α` where left-closed right-infinite intervals are closed, if `a` is an element of type `α`, then the left-closed right-infinite interval starting at `a`, denoted `Set.Ici a`, is a closed set in the topological space `α`. In other terms, this theorem asserts that under these conditions, the set of all elements `x` in `α` such that `a ≤ x` forms a closed set.
More concisely: Given a topological space `α` with a total order and a ClosedIciTopology where left-closed right-infinite intervals are closed, the left-closed right-infinite interval `Set.Ici a` is a closed set for any element `a` in `α`.
|
Ioi_mem_nhds
theorem Ioi_mem_nhds :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : ClosedIicTopology α] {a b : α},
a < b → Set.Ioi a ∈ nhds b
This theorem states that for any given type `α` which has a topological space structure, a linear order and a topology where the lower bounded closed intervals are closed, and for any two elements `a` and `b` of `α`, if `a` is strictly less than `b`, then the left-open right-infinite interval greater than `a` is a neighborhood of `b`. In mathematical terms, if $a < b$, then the set of all elements greater than $a$ is a neighborhood of $b$ in the topological space.
More concisely: For any topological space `α` endowed with a linear order and a topology where lower bounded closed intervals are closed, the left-open right-infinite interval around an element `a` is a neighborhood of any element `b` strictly greater than `a`.
|
Ioo_mem_nhdsWithin_Ioi
theorem Ioo_mem_nhdsWithin_Ioi :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : ClosedIciTopology α] {a b c : α},
b ∈ Set.Ico a c → Set.Ioo a c ∈ nhdsWithin b (Set.Ioi b)
This theorem states that for any types `α` which has a topological space structure, a linear order structure, and satisfies the `ClosedIciTopology` property, and for any three elements `a`, `b`, and `c` of type `α`, if `b` belongs to the left-closed right-open interval from `a` to `c` (`Set.Ico a c`), then the left-open right-open interval from `a` to `c` (`Set.Ioo a c`) is an element of the "neighborhood within" filter of `b` confined to the left-open right-infinite interval starting at `b` (`nhdsWithin b (Set.Ioi b)`).
In mathematical terms, if we have a topological space that also has a linear order and it satisfies the property that the set of all points greater than or equal to a given point is closed, then if `b` is in the interval `[a, c)`, the open interval `(a, c)` is in the neighborhood filter of `b` within the set of points greater than `b`.
More concisely: For any topological space `α` with a linear order and the `ClosedIciTopology` property, if `b` belongs to the left-closed right-open interval `[a, c)` in `α`, then `(a, c)` is in the neighborhood filter of `b` within the set of elements greater than `b`.
|
nhdsWithin_Ioo_eq_nhdsWithin_Iio
theorem nhdsWithin_Ioo_eq_nhdsWithin_Iio :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : ClosedIicTopology α] {a b : α},
a < b → nhdsWithin b (Set.Ioo a b) = nhdsWithin b (Set.Iio b)
This theorem states that for any type `α` that is a topological space, a linear order, and has a topology closed to the left (inclusive), if `a` and `b` are elements of `α` such that `a` is less than `b`, then the neighborhood within the open interval `(a, b)` at point `b` is equal to the neighborhood within the left-infinite open interval `(-∞, b)` at point `b`. In other words, the sets of neighborhoods of `b` that intersect with `(a, b)` and `(-∞, b)` respectively are the same when `a < b`.
More concisely: For any topological space and linear order `α` with `a < b` in `α`, the neighborhood filters of `b` in the open intervals `(a, b)` and `(-\infty, b)` coincide.
|
le_of_tendsto
theorem le_of_tendsto :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : ClosedIicTopology α]
{f : β → α} {a b : α} {x : Filter β} [inst_3 : x.NeBot],
Filter.Tendsto f x (nhds a) → (∀ᶠ (c : β) in x, f c ≤ b) → a ≤ b
The theorem `le_of_tendsto` states that for any types `α` and `β`, where `α` is a topological space with a preorder and a closed lower interval topology, and `β` is a filter that does not equal the bottom element, if a function `f` from `β` to `α` tends to a point `a` (i.e., for every neighborhood of `a`, the preimage of `f` is a neighborhood in the filter), and if almost every output of `f` is less than or equal to `b` for the filter `x` (i.e., this condition holds for all but a finite number of elements in `x`), then `a` is less than or equal to `b`. In other words, if a function `f` tends to a limit `a` and almost all its values are bounded by `b`, then `a` cannot be greater than `b`.
More concisely: If a function from a filter (not containing the bottom element) in a topological space with a preorder and closed lower interval topology, to another space, tends to a limit point and almost all its images are less than or equal to some bound, then the limit point is less than or equal to the bound.
|
closure_Iic
theorem closure_Iic :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : ClosedIicTopology α] (a : α),
closure (Set.Iic a) = Set.Iic a
This theorem states that for any type `α` that is a topological space and has a preorder, and if this type also has a topology where all left-infinite right-closed intervals are closed sets, then the closure of any left-infinite right-closed interval `Set.Iic a` is the interval itself. In mathematical terms, given any `a` in `α`, the closure of the set of all elements `x` such that `x ≤ a` is that same set.
More concisely: The closure of any left-infinite, right-closed interval in a topological preorder space is equal to the interval itself.
|
Iio_mem_nhds
theorem Iio_mem_nhds :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : ClosedIciTopology α] {a b : α},
a < b → Set.Iio b ∈ nhds a
The theorem `Iio_mem_nhds` states that for any type `α` with a topological space structure, a linear order, and a topology where left-closed right-open intervals are closed sets, and for any two elements `a` and `b` of `α`, if `a` is less than `b`, then the left-infinite right-open interval ending at `b` (denoted as `Set.Iio b`) is a neighborhood of `a`. This means that `Set.Iio b` contains an open set around `a`, or equivalently, it is included in the filter of neighborhoods of `a` (denoted as `nhds a`).
More concisely: For any topological space `α` with a linear order and a topology where left-closed right-open intervals are closed sets, if `a` is less than `b` in `α`, then the left-infinite right-open interval `Set.Iio b` is an element of the neighborhood filter `nhds a`.
|
le_of_tendsto_of_tendsto
theorem le_of_tendsto_of_tendsto :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α]
{f g : β → α} {b : Filter β} {a₁ a₂ : α} [inst_2 : b.NeBot],
Filter.Tendsto f b (nhds a₁) → Filter.Tendsto g b (nhds a₂) → b.EventuallyLE f g → a₁ ≤ a₂
This theorem, `le_of_tendsto_of_tendsto`, states that for any types `α` and `β` where `α` is a topological space, a preorder, and has an order-closed topology, if we have functions `f` and `g` from `β` to `α`, a filter `b` on `β` that is not the bottom filter, and two elements `a₁`, `a₂` of `α`, then if `f` tends to `a₁` along `b`, `g` tends to `a₂` along `b` and `f` is eventually less than or equal to `g` along `b`, then `a₁` is less than or equal to `a₂`.
In terms of limits, it says that if `f` and `g` are functions such that the limit of `f` as `β` approaches a point under a certain filter is `a₁`, the limit of `g` is `a₂`, and `f(β)` is less than or equal to `g(β)` for sufficiently large `β`, then `a₁` is less than or equal to `a₂`. This theorem is a formalization of the intuitive idea in calculus that if one function is eventually less than or equal to another, then the limit of the smaller function is less than or equal to the limit of the larger one.
More concisely: If `f` and `g` are functions from a filter `b` on a topological preorder `β` to a topological space `α` with order-closed topology, where `f` tends to `a₁` and `g` tends to `a₂` along `b`, and `f(x) ≤ g(x)` for all `x` in `β` that lie in the filter's limit points, then `a₁ ≤ a₂`.
|
Icc_mem_nhdsWithin_Ici
theorem Icc_mem_nhdsWithin_Ici :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : ClosedIciTopology α] {a b c : α},
b ∈ Set.Ico a c → Set.Icc a c ∈ nhdsWithin b (Set.Ici b)
This theorem states that for any type `α` that has a topological space structure, a linear order, and a topology where left-closed right-infinite intervals are closed, given any three elements `a`, `b`, and `c` of `α`, if `b` is in the left-closed right-open interval from `a` to `c` (i.e., `a ≤ b < c`), then the left-closed right-closed interval from `a` to `c` (i.e., `a ≤ x ≤ c`) is in the "neighborhood within" filter of `b` with respect to the left-closed right-infinite interval starting from `b` (i.e., `b ≤ x`). In simpler terms, this theorem is about a certain containment relationship involving intervals and a specific type of neighborhood in a specific type of topological space.
More concisely: If `α` is a type with a topology where left-closed right-infinite intervals are closed, and `a`, `b`, and `c` are elements of `α` with `a ≤ b < c`, then the left-closed right-closed interval from `a` to `c` is in the neighborhood filter of `b` with respect to the left-closed right-infinite interval starting from `b`.
|
isClosed_Iic
theorem isClosed_Iic :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : ClosedIicTopology α] {a : α},
IsClosed (Set.Iic a)
The theorem `isClosed_Iic` states that for any type `α` equipped with a topology and a preorder, and under the condition that the type has a closed left-infinite right-closed interval (`ClosedIicTopology`), then for any element `a` of type `α`, the left-infinite right-closed interval up to `a` (`Set.Iic a`) is a closed set in the topological space. In other words, it confirms that for any given point in the ordered topological space, the set of all points less than or equal to that point forms a closed set.
More concisely: If `α` is a type equipped with a topology and a preorder, and `α` has a closed left-infinite right-closed interval topology, then for any `a` in `α`, the set `Set.Iic a` of all points less than or equal to `a` is a closed set.
|
eventually_le_of_tendsto_lt
theorem eventually_le_of_tendsto_lt :
∀ {α : Type u} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : ClosedIciTopology α]
{l : Filter γ} {f : γ → α} {u v : α}, v < u → Filter.Tendsto f l (nhds v) → ∀ᶠ (a : γ) in l, f a ≤ u
This theorem, `eventually_le_of_tendsto_lt`, states that for any types `α` and `γ`, given a topological space and a linear order on `α`, a filter `l` on `γ`, a function `f` from `γ` to `α`, and two elements `u` and `v` of `α` such that `v` is less than `u`, if `f` tends to the neighborhood filter at `v` as the filter `l` varies, then for almost all `a` in `l`, the value `f(a)` is less than or equal to `u`. In mathematical terms, it says that if $f$ converges to $v$ under the filter $l$, and $v < u$, then $f(a) \leq u$ for almost all $a$ in the filter $l$.
More concisely: If a function $f: \gamma \to \alpha$ converges to $v$ in $\alpha$ with respect to a filter $l$ on $\gamma$, and $v < u$ in $\alpha$, then $f(a) \leq u$ for almost all $a$ in $l$.
|
interior_Ioi
theorem interior_Ioi :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : ClosedIicTopology α] {a : α},
interior (Set.Ioi a) = Set.Ioi a
This theorem states that for any type `α` equipped with a topological space structure, a linear order, and a topology where the half-closed, right-infinite intervals are closed, and a given element `a` of type `α`, the interior of the set of all elements greater than `a` is exactly the set itself. In other words, the set of all elements strictly greater than `a` is an open set in this topology.
More concisely: For any type `α` endowed with a topological space structure, a linear order, and a topology where right-open, half-closed intervals are closed, the set of elements strictly greater than a given `a` in `α` is the interior of this set in the topology.
|
continuous_if_le
theorem continuous_if_le :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : LinearOrder α]
[inst_2 : OrderClosedTopology α] {f g : β → α} [inst_3 : TopologicalSpace β] [inst_4 : TopologicalSpace γ]
[inst_5 : (x : β) → Decidable (f x ≤ g x)] {f' g' : β → γ},
Continuous f →
Continuous g →
ContinuousOn f' {x | f x ≤ g x} →
ContinuousOn g' {x | g x ≤ f x} →
(∀ (x : β), f x = g x → f' x = g' x) → Continuous fun x => if f x ≤ g x then f' x else g' x
The theorem `continuous_if_le` states that given topological spaces `α`, `β`, and `γ`, and functions `f` and `g` from `β` to `α` (with `α` having a linear order and order-closed topology), if `f` is continuous, `g` is continuous, and the functions `f'` and `g'` from `β` to `γ` are continuous on the sets where `f` is less than or equal to `g` and `g` is less than or equal to `f`, respectively, and for all `x` in `β`, whenever `f(x)` equals `g(x)`, `f'(x)` also equals `g'(x)`, then the function that maps `x` to `f'(x)` if `f(x)` is less than or equal to `g(x)` (otherwise `g'(x)`) is continuous.
More concisely: If functions `f` and `g` from a topological space `β` to an order-closed space `α` are continuous, `f` is less than or equal to `g` where both are defined, `g` is continuous at points where `f = g`, and `f'(x) = g'(x)` whenever `f(x) = g(x)`, then the function that maps `x` to `f'(x)` if `f(x) ≤ g(x)` and `g'(x)` otherwise is continuous.
|
ge_of_tendsto
theorem ge_of_tendsto :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : ClosedIciTopology α]
{f : β → α} {a b : α} {x : Filter β} [inst_3 : x.NeBot],
Filter.Tendsto f x (nhds a) → (∀ᶠ (c : β) in x, b ≤ f c) → b ≤ a
This theorem states that for any types `α` and `β`, where `α` is endowed with a topological space structure, a preorder structure, and a topology that is closed on the interval `[a, +∞)`, given a function `f` from `β` to `α`, and given two elements `a` and `b` of type `α` and a filter `x` of type `β`, such that the filter `x` is not bottom (i.e., it is not the filter that contains every set), if the function `f` tends to the neighborhood filter of `a` along the filter `x` (meaning that for every neighborhood of `a`, the preimage of that neighborhood under `f` is eventually in `x`), and if eventually every element of the codomain of `f` in the filter `x` is greater than or equal to `b`, then `b` is less than or equal to `a`. In simpler terms, if values of `f` get arbitrarily close to `a` and are eventually all at least `b`, then `b` is at most `a`.
More concisely: If a function from a filter on a preordered topological space to another preordered topological space tends to a point and eventually maps every element in the filter to a value greater than or equal to another point, then the second point is less than or equal to the first.
|
Ioc_mem_nhdsWithin_Iic'
theorem Ioc_mem_nhdsWithin_Iic' :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : ClosedIicTopology α] {a b : α},
a < b → Set.Ioc a b ∈ nhdsWithin b (Set.Iic b)
This theorem states that for any two elements `a` and `b` of some type `α`, where `α` is endowed with a topological space structure, a linear order structure, and a closed-left-infinite-right-closed-interval (`ClosedIicTopology`) topology, if `a` is less than `b`, then the left-open right-closed interval from `a` to `b` (`Set.Ioc a b`) is an element of the "neighborhood within" filter of `b` in the right-closed left-infinite interval up to `b` (`nhdsWithin b (Set.Iic b)`).
In plain English, this means that if we have a space where we can talk about order and closeness, and we have two points `a` and `b` with `a` less than `b`, then the open interval from `a` to `b` is a "local" concept around `b` when considering all points less than or equal to `b`.
More concisely: For any topological space `α` endowed with a linear order and a `ClosedIicTopology`, if `a` is less than `b` in the linear order, then `Set.Ioc a b` is an element of the neighborhood filter `nhdsWithin b (Set.Iic b)`.
|
tendsto_le_of_eventuallyLE
theorem tendsto_le_of_eventuallyLE :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α]
{f g : β → α} {b : Filter β} {a₁ a₂ : α} [inst_2 : b.NeBot],
Filter.Tendsto f b (nhds a₁) → Filter.Tendsto g b (nhds a₂) → b.EventuallyLE f g → a₁ ≤ a₂
This theorem states that for any two functions `f` and `g` from a set `β` to a topological preordered set `α` with an order closed topology, if `f` and `g` both tend towards points `a₁` and `a₂` respectively in the neighborhood filter at `a₁` and `a₂` when applied to elements of a non-bottom filter `b` from `β`, and if it is almost always true in `b` that `f` is less than or equal to `g`, then `a₁` is less than or equal to `a₂`. This can be thought of as a form of comparison theorem for functions on topological spaces.
More concisely: If functions `f` and `g` from a non-bottom filter `b` in a set `β` to a topological preordered set `α` with order closed topology, tend towards points `a₁` and `a₂` respectively at `a₁` and `a₂`, and `f ≤ g` holds in `b` except for a set of measure zero, then `a₁ ≤ a₂`.
|
Ioc_mem_nhdsWithin_Ioi
theorem Ioc_mem_nhdsWithin_Ioi :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : ClosedIciTopology α] {a b c : α},
b ∈ Set.Ico a c → Set.Ioc a c ∈ nhdsWithin b (Set.Ioi b)
This theorem states that for any type `α` equipped with a topological space structure, a linear order structure, and a topology that is closed at the lower side of the set [i, ∞) for each i, and for any three elements `a`, `b`, and `c` of type `α`, if `b` belongs to the left-closed right-open interval from `a` to `c`, then the left-open right-closed interval from `a` to `c` belongs to the "neighborhood within" filter of `b` in the right-infinite set where every element is greater than `b`. In simpler words, if `b` is in the interval [a,c) then the interval (a,c] is in the neighborhood of `b` where all points are greater than `b`.
More concisely: If `α` is a type with a topological space structure, a linear order, and a right-continuous topology at the set (i, ∞) for each i, then for any `a`, `b`, and `c` in `α` with `b` in the interval [a, c), the interval (a, c] is in the neighborhood filter of `b`.
|
OrderClosedTopology.isClosed_le'
theorem OrderClosedTopology.isClosed_le' :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] [self : OrderClosedTopology α],
IsClosed {p | p.1 ≤ p.2}
The theorem `OrderClosedTopology.isClosed_le'` states that for any type `α` equipped with a topology and a preorder, in an order-closed topology, the set of all pairs `(x, y)` where `x` is less than or equal to `y` is a closed set.
More concisely: In an order-closed topology on a preordered type `α`, the set of pairs `{(x, y) | x ≤ y}` is closed.
|
ContinuousWithinAt.closure_le
theorem ContinuousWithinAt.closure_le :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α]
[inst_2 : TopologicalSpace β] {f g : β → α} {s : Set β} {x : β},
x ∈ closure s → ContinuousWithinAt f s x → ContinuousWithinAt g s x → (∀ y ∈ s, f y ≤ g y) → f x ≤ g x
This theorem, `ContinuousWithinAt.closure_le`, states that for any two functions `f` and `g` from a topological space `β` to a preordered, topologically closed space `α`, along with a subset `s` of `β` and a point `x` in the closure of `s`, if both `f` and `g` are continuous at `x` within `s`, and `f y` is less than or equal to `g y` for all `y` in `s`, then `f x` is less than or equal to `g x`.
More concisely: If `f` and `g` are continuous at a point `x` in the closure of a subset `s` of a topological space, `β`, such that `f(y) ≤ g(y)` for all `y` in `s`, then `f(x) ≤ g(x)`.
|
Ici_mem_nhds
theorem Ici_mem_nhds :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : ClosedIicTopology α] {a b : α},
a < b → Set.Ici a ∈ nhds b
The theorem `Ici_mem_nhds` states that for any types `α` that has a topological space structure, a linear order, and a topology where the intervals closed towards negative infinity are closed sets (`ClosedIicTopology`), and for any elements `a` and `b` of type `α`, if `a` is less than `b`, then the set of all elements greater than or equal to `a` (`Set.Ici a`) is a neighborhood of `b`. In other words, this set contains an open set around `b`. The set of all neighborhoods of `b` forms a filter, known as the neighborhood filter at `b`.
More concisely: For any type `α` with a topology, linear order, and closed intervals towards negative infinity, if `a` is less than `b` in `α`, then the set of elements greater than or equal to `a` is a neighborhood of `b` in the neighborhood filter at `b`.
|
Ioo_mem_nhdsWithin_Iio
theorem Ioo_mem_nhdsWithin_Iio :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : ClosedIicTopology α] {a b c : α},
b ∈ Set.Ioc a c → Set.Ioo a c ∈ nhdsWithin b (Set.Iio b)
This theorem states that for any type `α` equipped with a topology and a linear order, and any three elements `a`, `b`, and `c` of `α`, if `b` is in the left-open right-closed interval from `a` to `c`, then the left-open right-open interval from `a` to `c` is in the neighborhood within the left-infinite right-open interval at `b`, under the condition that `α` has the closed lower semi-infinite topology.
In simpler terms, it asserts that if `b` is strictly greater than `a` and less than or equal to `c`, then any "small enough" neighborhood of `b` that does not include `b` itself but only values less than `b`, will contain some values that are strictly greater than `a` and strictly less than `c`. The "small enough" is determined by the topology on `α` which is assumed to be a closed lower semi-infinite topology.
More concisely: Given a type `α` with a topology and linear order, if `b` is in the left-open right-closed interval between `a` and `c` in `α`, then there exists a neighborhood of `b` containing elements strictly between `a` and `c` under the assumption of the closed lower semi-infinite topology.
|
Icc_mem_nhdsWithin_Ioi
theorem Icc_mem_nhdsWithin_Ioi :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : ClosedIciTopology α] {a b c : α},
b ∈ Set.Ico a c → Set.Icc a c ∈ nhdsWithin b (Set.Ioi b)
The theorem `Icc_mem_nhdsWithin_Ioi` states that for any given types `α` with a topological space structure, a linear order and a closed left-inclusive right-unbounded (closed-ici) topology, and any elements `a`, `b`, `c` of type `α`, if `b` is in the left-closed right-open interval from `a` to `c` (denoted as `Set.Ico a c`), then the left-closed, right-closed interval from `a` to `c` (denoted as `Set.Icc a c`) is in the neighborhood of `b` within the set of all elements greater than `b` (denoted as `nhdsWithin b (Set.Ioi b)`).
In simpler terms, this theorem ensures that if a number `b` is in an interval that includes its lower limit `a` and excludes its upper limit `c`, then the entire interval from `a` to `c` which includes both ends, is within the neighborhood of `b` considering only the numbers greater than `b`.
More concisely: If `a < b < c` and `b` belongs to the interval `[a, c)`, then `[a, c]` is contained in the neighborhood of `b` in the upper half-open interval `(b, ∞)`.
|
le_of_tendsto_of_tendsto'
theorem le_of_tendsto_of_tendsto' :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α]
{f g : β → α} {b : Filter β} {a₁ a₂ : α} [inst_2 : b.NeBot],
Filter.Tendsto f b (nhds a₁) → Filter.Tendsto g b (nhds a₂) → (∀ (x : β), f x ≤ g x) → a₁ ≤ a₂
This theorem states that for any types `α` and `β`, given a topological space, a preorder, and an order-closed topology on `α`, two functions `f` and `g` from `β` to `α`, a filter `b` on `β`, and two elements `a₁` and `a₂` of `α`, if the filter `b` is not bottom, the limit of `f` at `b` is a neighborhood of `a₁`, the limit of `g` at `b` is a neighborhood of `a₂`, and for all `x` in `β`, `f(x)` is less than or equal to `g(x)`, then `a₁` is less than or equal to `a₂`. In other words, if `f` and `g` are functions such that `f(x)` is always less than or equal to `g(x)` for all `x` and both `f` and `g` tend to limits `a₁` and `a₂` at the same filter `b`, then the limit `a₁` of `f` is less than or equal to the limit `a₂` of `g`.
More concisely: If `f` and `g` are functions from a preordered set `β` to an order-closed topological space `α`, with `f(x) ≤ g(x)` for all `x`, and `a₁` and `a₂` are the limits of `f` and `g`, respectively, at a non-bottom filter `b`, then `a₁ ≤ a₂`.
|
Filter.Tendsto.max_right
theorem Filter.Tendsto.max_right :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderClosedTopology α]
{f : β → α} {l : Filter β} {a : α},
Filter.Tendsto f l (nhds a) → Filter.Tendsto (fun i => max a (f i)) l (nhds a)
This theorem states that for any types `α` and `β`, given `α` as a topological space with a linear order that is closed under taking limits (`OrderClosedTopology`), if we have a function `f` from `β` to `α`, a filter `l` on `β`, and a point `a` in `α`, then, if `f` tends to `a` with respect to the filter `l` (i.e., `Filter.Tendsto f l (nhds a)`), then the function that maps each element of the domain to the maximum of `a` and `f` of that element also tends to `a` with respect to the filter `l` (i.e., `Filter.Tendsto (fun i => max a (f i)) l (nhds a)`). In simpler terms, if `f` approaches `a` in the limit, then taking the maximum of `a` and `f` at each point also approaches `a` in the limit.
More concisely: If `f` tends to `a` with respect to filter `l` in a topological space `α` with an order-closed topology, then the function `g(x) = max(a, f(x))` also tends to `a` with respect to `l` in `α`.
|
isClosed_le_prod
theorem isClosed_le_prod :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α],
IsClosed {p | p.1 ≤ p.2}
The theorem `isClosed_le_prod` states that for any type `α` that has a topology (i.e., it is a topological space), a preorder (i.e., it has a relation that is reflexive and transitive), and an order-closed topology (i.e., the topology is such that the set of points less than or equal to a given point is always closed), the set of ordered pairs `(p.1, p.2)` where `p.1` is less than or equal to `p.2` is a closed set.
More concisely: Given a topological space `α` with a preorder and an order-closed topology, the set of ordered pairs `{(x, y) | x ≤ y}` is closed.
|
interior_Iio
theorem interior_Iio :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : ClosedIciTopology α] {a : α},
interior (Set.Iio a) = Set.Iio a
This theorem states that for any type `α` equipped with a topological space, a linear order, and a topology where every set of the form `{x | x ≥ a}` is closed, the interior of the set of elements that are strictly less than `a` (denoted as `Set.Iio a`) is equal to the set `Set.Iio a` itself. This means that the largest open subset of `Set.Iio a` (which is its interior) is the set `Set.Iio a` itself.
More concisely: For any type `α` endowed with a topological space, a linear order, and a topology where every set of the form `{x | x < a}` is closed, the interior of the set of elements strictly less than `a` (`Set.Iio a`) equals `Set.Iio a` itself.
|
ge_of_tendsto'
theorem ge_of_tendsto' :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : ClosedIciTopology α]
{f : β → α} {a b : α} {x : Filter β} [inst_3 : x.NeBot],
Filter.Tendsto f x (nhds a) → (∀ (c : β), b ≤ f c) → b ≤ a
This theorem states that given a topological space `α` with a preorder and a topology closed at the upper interval (`ClosedIciTopology`), a function `f` from `β` to `α`, two elements `a` and `b` of `α`, and a non-bottom filter `x` on `β`, if `f` tends to `a` at `x` (i.e., for every neighborhood of `a`, the preimage under `f` of this neighborhood is a neighborhood at `x`) and for every `c` in `β`, `b` is less than or equal to `f(c)`, then `b` is less than or equal to `a`. In other words, if a function's values are always greater than or equal to a certain number and the function tends to a limit, then the limit is at least as large as that number.
More concisely: If a function `f` from a preordered topological space `β` to a preordered topological space `α` with `ClosedIciTopology`, `f` tends to `a` at a non-bottom filter `x` and `b ≤ f(c)` for all `c` in `β`, then `b ≤ a`.
|
eventually_ge_of_tendsto_gt
theorem eventually_ge_of_tendsto_gt :
∀ {α : Type u} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : ClosedIicTopology α]
{l : Filter γ} {f : γ → α} {u v : α}, u < v → Filter.Tendsto f l (nhds v) → ∀ᶠ (a : γ) in l, u ≤ f a
The theorem `eventually_ge_of_tendsto_gt` states that for all types `α` and `γ`, with `α` having a topological space structure, a linear order, and a closed "left-hand limit" topology, given a filter `l` on `γ`, a function `f` from `γ` to `α`, and two elements `u` and `v` of `α` such that `u` is less than `v`, if the function `f` tends towards the neighborhood of `v` under the filter `l`, then there exists an eventuality (i.e., for all sufficiently large elements `a` of `γ` under the filter `l`), such that `u` is less than or equal to `f(a)`.
In simpler terms, if we have a function that tends towards a certain value, then beyond a certain point, the function's value will be greater than or equal to a given number that is strictly less than the value the function is tending to.
More concisely: Given a filter `l` on `γ`, a function `f` from `γ` to `α` (where `α` is a type with a topological space structure, a linear order, and a closed "left-hand limit" topology), and elements `u` and `v` of `α` with `u < v`, if `f` tends to the neighborhood of `v` under `l`, then there exists an eventuality `A` under `l` such that `u ≤ f(a)` for all `a` in `A`.
|
closure_Ici
theorem closure_Ici :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : ClosedIciTopology α] (a : α),
closure (Set.Ici a) = Set.Ici a
This theorem is a statement about sets and topologies in a mathematical context. Specifically, it states that for any type `α`, which is a topological space and a preorder (that is, it has a relation that is reflexive and transitive), and also has a topology where all left-closed right-infinite intervals are closed sets (`ClosedIciTopology α`), the closure of a left-closed right-infinite interval starting from a point `a` (`Set.Ici a`) is equal to the interval itself. In other words, the smallest closed set containing the interval `[a, ∞)` is the interval `[a, ∞)` itself.
More concisely: For any topological space and preorder type `α` with `ClosedIciTopology α`, the closure of a left-closed right-infinite interval `[a, ∞)` equals the interval itself.
|
isClosed_le
theorem isClosed_le :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α]
[inst_2 : TopologicalSpace β] {f g : β → α}, Continuous f → Continuous g → IsClosed {b | f b ≤ g b}
This theorem states that for any types `α` and `β`, given `α` is a topological space and a preorder with order-closed topology, and `β` is also a topological space, if `f` and `g` are two continuous functions from `β` to `α`, then the set of all elements `b` in `β` such that `f(b)` is less than or equal to `g(b)` is a closed set.
More concisely: If `α` is a topological space and a preorder with order-closed topology, and `β` is a topological space, then the set of elements `b` in `β` such that `f(b) ≤ g(b)` for continuous functions `f` and `g` from `β` to `α` forms a closed set in `β`.
|
nhdsWithin_Ioo_eq_nhdsWithin_Ioi
theorem nhdsWithin_Ioo_eq_nhdsWithin_Ioi :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : ClosedIciTopology α] {a b : α},
a < b → nhdsWithin a (Set.Ioo a b) = nhdsWithin a (Set.Ioi a)
This theorem, `nhdsWithin_Ioo_eq_nhdsWithin_Ioi`, states that for any type `α` equipped with a topological space structure, a linear order, and a topology such that the set of all elements greater than or equal to any given element is closed, if `a` and `b` are elements of `α` and `a` is less than `b`, then the "neighborhood within" filter of `a` with respect to the left-open right-open interval from `a` to `b` is equal to the "neighborhood within" filter of `a` with respect to the left-open right-infinite interval starting from `a`. In simpler terms, the local behavior of `a` in the interval `(a, b)` is the same as its local behavior in the interval `(a, +∞)`.
More concisely: For any topological space `α` with a linear order and the property that every upper set is closed, if `a` and `b` are elements of `α` with `a < b`, then the neighborhood filter of `a` in the interval `(a, b)` is equal to the neighborhood filter of `a` in the interval `(a, +∞)`.
|
frontier_le_subset_eq
theorem frontier_le_subset_eq :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderClosedTopology α]
{f g : β → α} [inst_3 : TopologicalSpace β],
Continuous f → Continuous g → frontier {b | f b ≤ g b} ⊆ {b | f b = g b}
This theorem states that for all types α and β with α being a type associated with a topological space, a linear order, and an order-closed topology, and β being a type associated with a topological space, and for all continuous functions f and g from β to α, the frontier (boundary) of the set of elements in β for which f(b) is less than or equal to g(b) is a subset of the set of elements in β for which f(b) equals g(b).
More concisely: For all continuous functions f and g from a topological space β with order-closed topology and type α, the boundary of the set where f < g equals the set where f = g.
|
Dense.orderDual
theorem Dense.orderDual :
∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α}, Dense s → Dense (⇑OrderDual.ofDual ⁻¹' s)
This theorem states that for any given type `α` with a topological space structure, and any given set `s` of that type, if `s` is a dense set in that topological space, then the pre-image of `s` under the function `OrderDual.ofDual` is also a dense set. In other words, if every point in the topological space belongs to the closure of `s`, then every point also belongs to the closure of the set obtained by applying the function `OrderDual.ofDual` to each element of `s`. This function is essentially the identity function on the dual order of `α`, making this a statement about the preservation of density under this particular function.
More concisely: If `α` is a topological space type with a dense set `s`, then the pre-image of `s` under the OrderDual.ofDual function is also dense.
|
isOpen_lt
theorem isOpen_lt :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderClosedTopology α]
[inst_3 : TopologicalSpace β] {f g : β → α}, Continuous f → Continuous g → IsOpen {b | f b < g b}
The theorem `isOpen_lt` states that for any two types `α` and `β`, where `α` has a topological space, a linear order, and an order-closed topology structure, and `β` has a topological space structure, for any two continuous functions `f` and `g` from `β` to `α`, the set of all `b` in `β` such that `f(b)` is less than `g(b)` is an open set in the topological space of `β`. This theorem links together concepts from topology and order theory, saying essentially that under certain conditions, the "less than" relation between the outputs of two continuous functions opens to an open set.
More concisely: For any continuous functions `f` and `g` between topological spaces `β` with order-closed topology and `α`, the set of `b` in `β` such that `f(b) < g(b)` is an open subset of `β`.
|
ClosedIciTopology.isClosed_ge'
theorem ClosedIciTopology.isClosed_ge' :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : ClosedIciTopology α] (a : α),
IsClosed {x | a ≤ x}
This theorem states that for any type `α` which has the structure of a topological space and a preorder, and satisfies the `ClosedIciTopology` condition (i.e., all sets of the form [a, ∞) are closed), a set that includes all elements `x` that are greater than or equal to a certain element `a` is a closed set.
More concisely: For any topological space and preordered type `α` satisfying the `ClosedIciTopology` condition, the set of elements greater than or equal to `a` is a closed set.
|
Iic_mem_nhds
theorem Iic_mem_nhds :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : ClosedIciTopology α] {a b : α},
a < b → Set.Iic b ∈ nhds a
This theorem states that for any types `α` that have a topological space structure, a linear order structure, and a topology where the set of numbers greater than or equal to a particular number is closed, if `a` and `b` are elements of `α` with `a` less than `b`, then the set of all elements less than or equal to `b` is a neighborhood of `a`. In other words, the left-infinite right-closed interval up to `b` is in the neighborhood filter of `a`.
More concisely: For any type `α` endowed with a topology, a linear order, and the property that the set of elements greater than or equal to any given element is closed, if `a` is less than `b` in `α`, then the set of elements less than or equal to `b` is a neighborhood of `a`.
|
eventually_lt_nhds
theorem eventually_lt_nhds :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : ClosedIciTopology α] {a b : α},
a < b → ∀ᶠ (x : α) in nhds a, x < b
This theorem states that for any type `α` that is a topological space with a linear order, and for which the topology is generated by right-closed intervals (expressed by `ClosedIciTopology α`), given any two elements `a` and `b` of `α` such that `a < b`, then eventually (meaning in the neighborhood filter or `nhds` of `a`), all elements `x` will be less than `b`. This is essentially a property about the limit behavior of elements in a topological space with these specific properties.
More concisely: In a topological space `α` with a linear order and a topology generated by right-closed intervals, if `a < b` then every neighborhood of `a` contains only elements less than `b`.
|
Continuous.max
theorem Continuous.max :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderClosedTopology α]
{f g : β → α} [inst_3 : TopologicalSpace β], Continuous f → Continuous g → Continuous fun b => max (f b) (g b)
This theorem states that for any two continuous functions `f` and `g` mapping from a topological space `β` to a linearly ordered topological space `α` with an order-closed topology, the function that sends each element of `β` to the maximum of the corresponding elements in `f` and `g` is also continuous. In other words, if `f` and `g` are continuous functions, then the function that takes a point `b` in `β` and maps it to the greater of `f(b)` and `g(b)` is also continuous.
More concisely: If `f` and `g` are continuous functions mapping from a topological space `β` to a linearly ordered topological space `α` with order-closed topology, then the function that maps each point `b` in `β` to the maximum of `f(b)` and `g(b)` is also continuous.
|
not_tendsto_nhds_of_tendsto_atTop
theorem not_tendsto_nhds_of_tendsto_atTop :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : NoTopOrder α] [inst_2 : TopologicalSpace α]
[inst_3 : ClosedIciTopology α] {l : Filter β} [inst_4 : l.NeBot] {f : β → α},
Filter.Tendsto f l Filter.atTop → ∀ (a : α), ¬Filter.Tendsto f l (nhds a)
This theorem states that for any types `α` and `β`, where `α` is a preorder without a top element, endowed with a topology for which every set of the form `{b | a ≤ b}` is closed, and `β` is associated with a filter `l` that is not the bottom filter, if a function `f` from `β` to `α` tends towards infinity (i.e., for any `b` in `β`, `f(b)` is arbitrarily large), then `f` cannot tend towards any particular value `a` in `α`. In other words, if the values of `f` become arbitrarily large as its argument changes according to the filter `l`, then `f` cannot settle down to any specific value.
More concisely: Given a preorder `α` without a top element, endowed with a topology where every upper set is closed, and a filter `l` on a type `β` such that `l` is not the bottom filter, any function `f : β → α` that tends towards infinity cannot converge to any specific value in `α`.
|
isOpen_Ioi
theorem isOpen_Ioi :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : ClosedIicTopology α] {a : α},
IsOpen (Set.Ioi a)
The theorem `isOpen_Ioi` states that for any type `α` which is equipped with a topological space, a linear order, and a topology in which the sets of the form `(-∞, b]` (denoted as `ClosedIicTopology`) are closed, the set of all elements greater than a given element `a` (denoted as `Set.Ioi a`) is an open set in this topology. In the context of real numbers, this means the open interval `(a, ∞)` is considered an open set in the given topological space.
More concisely: For any type `α` with a topological space, linear order, and `ClosedIicTopology`, the set `{x : α | x > a}` is open.
|
isOpen_Iio
theorem isOpen_Iio :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : ClosedIciTopology α] {a : α},
IsOpen (Set.Iio a)
The theorem `isOpen_Iio` states that for any type `α` that is equipped with a topological space structure, a linear order structure, and a topology where the "closed and bounded at the top" sets are closed, if `a` is an element of `α`, then the left-infinite right-open interval `{x | x < a}` (denoted as `Set.Iio a`) is an open set in the ambient topological space on `α`. That is, the set of all elements less than `a` forms an open set in this particular topology.
More concisely: Given a topological space `(α, top)` with a linear order `<` and `a ∈ α` such that the closed and bounded sets are topologically closed, the set `{x | x < a}` is open.
|
Ioo_mem_nhds
theorem Ioo_mem_nhds :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderClosedTopology α] {a b x : α},
a < x → x < b → Set.Ioo a b ∈ nhds x
This theorem, `Ioo_mem_nhds`, states that for any type `α` that is a topological space, is a linear order, and has an order-closed topology, and for any `a`, `b`, and `x` of type `α`, if `a` is less than `x` and `x` is less than `b`, then the open interval `(a, b)` (represented by `Set.Ioo a b`), is a neighborhood of `x` (i.e., it belongs to the neighborhood filter at `x` denoted by `nhds x`). In other words, within these given structures, if `x` lies strictly between `a` and `b`, then the open interval from `a` to `b` forms a neighborhood around `x`.
More concisely: If `α` is a topological space, a linear order with an order-closed topology, then for all `a < x < b` in `α`, `Set.Ioo a b` is a neighborhood of `x`.
|
Icc_mem_nhds
theorem Icc_mem_nhds :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderClosedTopology α] {a b x : α},
a < x → x < b → Set.Icc a b ∈ nhds x
This theorem states that for any types `α` with a topology, a linear order, and an order-closed topology, and for any elements `a`, `b`, and `x` of type `α`, if `x` is strictly between `a` and `b`, then the closed interval from `a` to `b` (`Set.Icc a b`) is a neighborhood of `x`. In other words, the interval `[a, b]` contains an open set around `x` and as such is part of the filter of neighborhoods of `x` (`nhds x`).
More concisely: For any type `α` with a topology, a linear order, and an order-closed topology, if `x` strictly lies between `a` and `b` in `α`, then the closed interval `[a, b]` is a neighborhood of `x`.
|
isClosed_Icc
theorem isClosed_Icc :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α] {a b : α},
IsClosed (Set.Icc a b)
This theorem, `isClosed_Icc`, states that for any type `α` that is equipped with a topological space structure, a preorder structure, and an order-closed topology, the interval `[a, b]` (i.e., the set of all `x` such that `a ≤ x ≤ b`) is a closed set. Here, `a` and `b` are arbitrary elements of type `α`. An order-closed topology is a specific type of topology where any set that is closed under taking limits from the right and left is defined as a closed set.
More concisely: In a topological space equipped with a preorder and an order-closed topology, the interval [a, b] is a closed set for all a ≤ b in the preorder.
|
not_tendsto_atTop_of_tendsto_nhds
theorem not_tendsto_atTop_of_tendsto_nhds :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : NoTopOrder α] [inst_2 : TopologicalSpace α]
[inst_3 : ClosedIciTopology α] {a : α} {l : Filter β} [inst_4 : l.NeBot] {f : β → α},
Filter.Tendsto f l (nhds a) → ¬Filter.Tendsto f l Filter.atTop
This theorem states that for any types `α` and `β`, if `α` has a preorder and there is no top element, and `α` is also topological space with a closed Ici topology, then given an element `a` of `α`, a filter `l` over `β` which is not the bottom filter, and a function `f` from `β` to `α`, if the function `f` satisfies the condition that the limit as `f` approaches `l` is a neighborhood of `a` (i.e., `Filter.Tendsto f l (nhds a)`), then it cannot be the case that the function `f` also tends to infinity at `l` (i.e., `¬Filter.Tendsto f l Filter.atTop`).
In simpler terms, for a given function, if the limit of the function at a certain point is a certain value, then the function cannot also tend to infinity at that point.
More concisely: If `α` is a preorder without a top element, a topological space with a closed Ici topology, and `f: β -> α` satisfies `Filter.Tendsto f l (nhds a)`, then `¬Filter.Tendsto f l Filter.atTop`.
|
Ico_mem_nhdsWithin_Ici'
theorem Ico_mem_nhdsWithin_Ici' :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : ClosedIciTopology α] {a b : α},
a < b → Set.Ico a b ∈ nhdsWithin a (Set.Ici a)
This theorem states that for any type `α` that has a topological space structure, a linear order structure, and a right-closed interval topology, and for any two elements `a` and `b` of this type where `a` is less than `b`, the half-open interval from `a` to `b` (i.e., the set of all `x` such that `a` is less than or equal to `x` and `x` is less than `b`) is a member of the "neighborhood within" filter of `a` restricted to the set of all elements greater than or equal to `a`. In other words, the half-open interval from `a` to `b` is a neighborhood of `a` within the set of all elements greater than or equal to `a`. The "neighborhood within" filter is a concept from topology that describes the local behavior of a point within a certain set; in this case, the set of all elements greater than or equal to `a`.
More concisely: For any type `α` with a topological space, linear order, and right-closed interval topology structure, the half-open interval from `a` to `b` (where `a` is less than `b`) is a neighborhood of `a` within the set of elements greater than or equal to `a`.
|
disjoint_nhds_atTop
theorem disjoint_nhds_atTop :
∀ {α : Type u} [inst : Preorder α] [inst_1 : NoTopOrder α] [inst_2 : TopologicalSpace α]
[inst_3 : ClosedIciTopology α] (a : α), Disjoint (nhds a) Filter.atTop
This theorem, `disjoint_nhds_atTop`, states the following: for any type `α` which is a `Preorder` and a `TopologicalSpace`, and for which there is no top order (`NoTopOrder`) and the topology is closed on the interval from a given value to infinity (`ClosedIciTopology`), the neighborhood filter (`nhds`) at any value `a` and the filter representing the limit towards infinity (`Filter.atTop`) are disjoint. This means that their infimum is the bottom element, generalizing the concept of disjoint sets. In more mathematical terms, for any element `x` that is less than or equal to `a` and is also in the limit towards infinity, `x` is less than or equal to the bottom element.
More concisely: For any Preorder and TopologicalSpace α without a top order and with a ClosedIciTopology, the neighborhood filter at any point a is disjoint from the filter representing the limit towards infinity, i.e., their infimum is the bottom element.
|
disjoint_nhds_atBot
theorem disjoint_nhds_atBot :
∀ {α : Type u} [inst : Preorder α] [inst_1 : NoBotOrder α] [inst_2 : TopologicalSpace α]
[inst_3 : ClosedIicTopology α] (a : α), Disjoint (nhds a) Filter.atBot
This theorem states that for any type `α` that has a preorder structure, does not have a minimal element (NoBotOrder), has a topological structure, and where the interval semi-open to the left (ClosedIicTopology) is a closed set, the neighborhood filter at an element `a` of `α` (denoted as `nhds a`) and the filter representing the limit towards negative infinity (`Filter.atBot`) are disjoint. Disjointness here means that their infimum is the bottom element. In other words, there is no common smaller element between a neighborhood of `a` and the set of all elements that are less than or equal to any given element in the type `α`.
More concisely: For any type `α` with a NoBotOrder preorder, a topology making ClosedIicTopology intervals closed, and without a minimal element, the neighborhood filter of an element `a` is disjoint from the filter representing the limit towards negative infinity, i.e., their infimum is the bottom element.
|
Continuous.min
theorem Continuous.min :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderClosedTopology α]
{f g : β → α} [inst_3 : TopologicalSpace β], Continuous f → Continuous g → Continuous fun b => min (f b) (g b)
This theorem states that for any two given continuous functions `f` and `g` mapping from type `β` to a type `α` (which is equipped with a topological space structure, linear order, and an order-closed topology), the function that takes an input `b` of type `β` and returns the minimum value between `f(b)` and `g(b)` is also a continuous function. Here, continuity is defined under the topological space structure of `α` and `β`.
More concisely: Given continuous functions `f` and `g` from a topological space `β` to a topologically ordered and order-closed space `α`, the function that maps each `b` in `β` to the minimum of `f(b)` and `g(b)` is also continuous.
|
isOpen_Ioo
theorem isOpen_Ioo :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderClosedTopology α] {a b : α},
IsOpen (Set.Ioo a b)
The theorem `isOpen_Ioo` states that for any type `α` with a topological space structure, a linear order structure, and an order-closed topology structure, the open interval `(a, b)`, represented in Lean 4 as `Set.Ioo a b`, is an open set in the given topological space. In other words, every interval `(a, b)` is open in any topological space that is also a linearly ordered space with order-closed topology.
More concisely: In any topological space endowed with a linear order and an order-closed topology, the open interval (a, b) is an open set.
|
frontier_Iic_subset
theorem frontier_Iic_subset :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderClosedTopology α] (a : α),
frontier (Set.Iic a) ⊆ {a}
The theorem `frontier_Iic_subset` asserts that for all types `α` equipped with a topological space structure, a linear order structure, and an order-closed topology structure, for any element `a` of type `α`, the frontier of the left-infinite right-closed interval ending at `a` is a subset of the set that contains only `a`. In other words, the only boundary point of the interval from negative infinity to `a` inclusive, in a space with these structures, is `a` itself.
More concisely: For any type `α` with a topological space, linear order, and order-closed topology structures, the frontier of the left-infinite right-closed interval in this structure is equal to the singleton set containing the endpoint `a`.
|
IsClosed.isClosed_le
theorem IsClosed.isClosed_le :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α]
[inst_2 : TopologicalSpace β] {f g : β → α} {s : Set β},
IsClosed s → ContinuousOn f s → ContinuousOn g s → IsClosed {x | x ∈ s ∧ f x ≤ g x}
This theorem states that if we have a set `s` that is closed in a topological space, and `f` and `g` are functions that are continuous on `s`, then the set of points `x` in `s` such that `f(x)` is less than or equal to `g(x)` is also a closed set. Here, `α` and `β` are types equipped with a topological structure, `α` is also equipped with an order relation and an order-closed topology. The functions `f` and `g` map from `β` to `α`. The `IsClosed` predicate checks whether a set is closed in its topological space.
More concisely: If `s` is a closed subset of a topological space `(α, τ)` with order relation `≤`, and `f` and `g` are continous functions from `(β, τ')` to `(α, τ)` such that `f(x) ≤ g(x)` for all `x ∈ s`, then the set `{x ∈ s | f(x) ≤ g(x)}` is closed in `(α, τ)`.
|
ClosedIicTopology.isClosed_le'
theorem ClosedIicTopology.isClosed_le' :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : ClosedIicTopology α] (a : α),
IsClosed {x | x ≤ a}
This theorem states that for any type `α` that has a topology, a preorder (which is a binary relation indicating that for any two elements `x` and `y`, either `x` precedes `y`, `y` precedes `x`, or `x` and `y` are equivalent), and a closed (lower) interval topology, and for any element `a` of type `α`, the set of all elements `x` such that `x` is less than or equal to `a` is a closed set in this topological space.
More concisely: For any topological space $(X,\tau)$ where $X$ is a type equipped with a topology $\tau$, a preorder relation, and a closed interval topology, the set of elements less than or equal to a given element is closed. That is, $\forall a\in X, \ \ \{x\in X\ |\ x\leq a\}\in \tau$.
|