exists_seq_strictMono_tendsto
theorem exists_seq_strictMono_tendsto :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] [inst_4 : NoMinOrder α] [inst_5 : FirstCountableTopology α] (x : α),
∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Filter.Tendsto u Filter.atTop (nhds x)
The theorem `exists_seq_strictMono_tendsto` states that for any point `x` in a topological space `α`, which is also a linear order where the order topology is assumed, densely ordered with no minimal element and having a first-countable topology, there exists a sequence `u` that is strictly monotonically increasing (meaning each term `u n` is less than `u (n+1)`) and all terms of `u` are less than `x`. Moreover, this sequence `u` converges to `x` as it tends to infinity. In other words, arbitrarily large terms of `u` get arbitrarily close to `x`.
More concisely: Given a densely ordered, first-countable linear space `α` without a minimal element, there exists a strictly monotonically increasing sequence `u` such that `u(n)` converges to any `x` in `α` as `n` tends to infinity.
|
IsLUB.frequently_mem
theorem IsLUB.frequently_mem :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α] {a : α}
{s : Set α}, IsLUB s a → s.Nonempty → ∃ᶠ (x : α) in nhdsWithin a (Set.Iic a), x ∈ s
This theorem, `IsLUB.frequently_mem`, states that for any type `α` that has a topological space structure, a linear order, and an order topology, any set `s` of this type `α`, and any element `a` of type `α`, if `a` is a least upper bound of the set `s` and the set `s` is not empty, then there frequently exists an element `x` in the intersection of the left-closed right-infinite interval up to `a` and a neighborhood of `a`, such that `x` is an element of the set `s`. In other words, if `a` is the least upper bound of a non-empty set, then there are many elements in `s` arbitrarily close to `a` but not greater than `a`.
More concisely: For any non-empty set `s` of a type `α` with a topological space structure, linear order, and order topology, if `a` is the least upper bound of `s`, then there exists an element `x` in the intersection of the left-closed right-infinite interval up to `a` and a neighborhood of `a` that belongs to `s`.
|
IsGLB.mem_of_isClosed
theorem IsGLB.mem_of_isClosed :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α] {a : α}
{s : Set α}, IsGLB s a → s.Nonempty → IsClosed s → a ∈ s
This theorem states that for any type `α` where `α` is a topological space, a linear order, and an order topology, and for any element `a` of type `α` and set `s` of type `α`, if `a` is a greatest lower bound of the set `s`, the set `s` is not empty, and the set `s` is closed, then `a` belongs to the set `s`. In mathematical terms, this theorem asserts that if a set in a topological space has a greatest lower bound and is not empty and closed, then the greatest lower bound is an element of the set.
More concisely: In a topological space endowed with a linear order and order topology, if a non-empty, closed set has a greatest lower bound, then that bound is an element of the set.
|
IsClosed.isGLB_mem
theorem IsClosed.isGLB_mem :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α] {a : α}
{s : Set α}, IsGLB s a → s.Nonempty → IsClosed s → a ∈ s
This theorem state that for any type `α` equipped with a topology (`TopologicalSpace α`), a linear order (`LinearOrder α`), and an order topology (`OrderTopology α`), and for any set `s` of type `α` and an element `a` of type `α`, if `a` is a greatest lower bound of the set `s`, and if `s` is nonempty and closed in the topology, then `a` is an element of the set `s`. In simpler words, the greatest lower bound of a nonempty closed set in a topological space with a linear order and an order topology is always an element of the set.
More concisely: If `α` is a type with a topology, a linear order, and an order topology, and `s` is a nonempty closed subset of `α` with greatest lower bound `a` in the order, then `a` is an element of `s`.
|
IsGLB.mem_closure
theorem IsGLB.mem_closure :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α] {a : α}
{s : Set α}, IsGLB s a → s.Nonempty → a ∈ closure s
This theorem states that for any type `α` that has a topology, a linear order structure, and an order topology, given a set `s` of type `α` and an element `a` of type `α`, if `a` is a greatest lower bound of `s` and `s` is nonempty, then `a` belongs to the closure of `s`. The closure of a set `s` is the smallest closed set containing `s`. This theorem essentially describes a property of the closure of a set in a topological space with a linear order structure.
More concisely: If a nonempty set `s` in a topological space `α` with a linear order structure has a greatest lower bound `a`, then `a` belongs to the closure of `s`.
|
IsLUB.mem_closure
theorem IsLUB.mem_closure :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α] {a : α}
{s : Set α}, IsLUB s a → s.Nonempty → a ∈ closure s
This theorem, `IsLUB.mem_closure`, states that for any type `α` that is a topological space and also a linear order with an order topology, and for any set `s` of elements of type `α` and an element `a` of type `α`, if `a` is the least upper bound of the set `s` and if the set `s` is not empty, then `a` is an element of the closure of the set `s`. In other words, the least upper bound of a non-empty set belongs to the closure of that set in a linearly ordered topological space.
More concisely: In a linearly ordered topological space, the least upper bound of any non-empty set is an element of the closure of that set.
|
exists_seq_strictAnti_tendsto
theorem exists_seq_strictAnti_tendsto :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] [inst_4 : NoMaxOrder α] [inst_5 : FirstCountableTopology α] (x : α),
∃ u, StrictAnti u ∧ (∀ (n : ℕ), x < u n) ∧ Filter.Tendsto u Filter.atTop (nhds x)
This theorem states that for any type `α` that has a topology, a linear order, an order topology, is densely ordered, has no maximum order, and a first countable topology, and for any element `x` of type `α`, there exists a sequence `u` that meets the following conditions:
- `u` is strictly antitone, i.e., if `a < b` then `u b < u a`.
- For all natural numbers `n`, `x` is less than `u n`.
- The sequence `u` tends to `x` as it goes to infinity, i.e., for every open set around `x`, all but finitely many elements of the sequence `u` are in that open set.
More concisely: For any densely ordered, first countable, no-maximum, topological space `(α, ≤, top)` with order topology, there exists a strictly antitone sequence `{u_n}` in `α` such that `x ≤ u_n` for all `n` and `x` is the limit of `{u_n}` as `n` approaches infinity.
|
IsLUB.nhdsWithin_neBot
theorem IsLUB.nhdsWithin_neBot :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α] {a : α}
{s : Set α}, IsLUB s a → s.Nonempty → (nhdsWithin a s).NeBot
The theorem `IsLUB.nhdsWithin_neBot` states that for any type `α` that has a topological structure, a linear ordering, and an order topology, and for any element `a` of type `α` and set `s` of type `α`, if `a` is a least upper bound of `s` and the set `s` is not empty, then the filter generated by the intersection of `s` and a neighborhood of `a` (expressed as `nhdsWithin a s`) is not bottom, meaning it contains at least one set other than the empty set. This theorem is important in the study of topology and order theory, and it implies that the intersection of `s` with any neighborhood of a least upper bound of `s` is always nonempty.
More concisely: For any non-empty set `s` with a least upper bound `a` in a topological order `α`, the filter generated by `s` and a neighborhood of `a` is non-empty.
|
IsClosed.isLUB_mem
theorem IsClosed.isLUB_mem :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α] {a : α}
{s : Set α}, IsLUB s a → s.Nonempty → IsClosed s → a ∈ s
This theorem, also known as `IsClosed.isLUB_mem`, states that for any type `α` which has a Topological Space structure, a Linear Order structure, and an Order Topology structure, if `a` is a least upper bound (LUB) of a set `s` and `s` is nonempty and closed, then `a` belongs to `s`. In other words, if a set is nonempty and closed in order topology, its least upper bound is a member of the set itself.
More concisely: If a nonempty, closed set in a topological space with a linear order and order topology has a least upper bound, then that bound belongs to the set.
|
IsLUB.mem_of_isClosed
theorem IsLUB.mem_of_isClosed :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α] {a : α}
{s : Set α}, IsLUB s a → s.Nonempty → IsClosed s → a ∈ s
This theorem, referred to as `IsLUB.mem_of_isClosed`, is stating that for any given type `α` equipped with a topology, a linear order, and an order topology, if `a` is the least upper bound of a set `s` and `s` is non-empty and closed, then the element `a` is a member of the set `s`. In other words, if a non-empty set `s` in a topological space is closed, its least upper bound (if it exists) is an element of the set `s`.
More concisely: If `s` is a non-empty, closed subset of a topological space equipped with a linear order, then its least upper bound (if it exists) is an element of `s`.
|
IsLUB.isLUB_of_tendsto
theorem IsLUB.isLUB_of_tendsto :
∀ {α : Type u_1} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : Preorder γ] [inst_4 : TopologicalSpace γ] [inst_5 : OrderClosedTopology γ] {f : α → γ} {s : Set α}
{a : α} {b : γ},
MonotoneOn f s → IsLUB s a → s.Nonempty → Filter.Tendsto f (nhdsWithin a s) (nhds b) → IsLUB (f '' s) b
The theorem `IsLUB.isLUB_of_tendsto` in Lean 4 states that for any types `α` and `γ`, given a topological space structure on `α`, a linear order on `α`, an order topology on `α`, a preorder on `γ`, a topological space structure on `γ`, and an order-closed topology on `γ`, along with a function `f` from `α` to `γ`, a set `s` of type `α`, and elements `a` of type `α` and `b` of type `γ`, if the function `f` is monotone on the set `s`, `a` is a least upper bound of the set `s`, the set `s` is nonempty, and `f` tends to `b` within `s` near `a`, then `b` is a least upper bound of the image of `s` under `f`.
In simpler terms, if we have a function `f` that is monotone on a nonempty set `s`, and `a` is a least upper bound of `s`, then if the function `f` continues to approach `b` as `f`s values get closer and closer to `a` within `s`, `b` will be the least upper bound of the values of `f` at `s`. This theorem is a bridging result between order theory and topology, which are two important branches of mathematics.
More concisely: If `f` is a monotone function from a nonempty, order-closed set `s` with a least upper bound `a` in a topological space `α` with an order topology, and `f(a)` is a limit point of `f(s)` as `x` approaches `a` in `α`, then `f(a)` is the least upper bound of `f(s)`.
|
IsLUB.exists_seq_strictMono_tendsto_of_not_mem
theorem IsLUB.exists_seq_strictMono_tendsto_of_not_mem :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α] {t : Set α} {x : α}
[inst_3 : (nhds x).IsCountablyGenerated],
IsLUB t x →
x ∉ t →
t.Nonempty →
∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Filter.Tendsto u Filter.atTop (nhds x) ∧ ∀ (n : ℕ), u n ∈ t
This theorem states that for any topological linear ordered space `α` with order topology and a neighborhood filter `nhds x` that is countably generated, given a set `t` in `α` and an element `x` in `α` such that `x` is a least upper bound of `t` but does not belong to `t`, and provided that `t` is not empty, there exists a sequence `u` with the following properties:
1. `u` is strictly increasing.
2. Every term `u n` of sequence `u` is less than `x`.
3. `u` tends to `x` as `n` tends to infinity.
4. Every term `u n` of sequence `u` belongs to `t`.
In simpler terms, if you have a non-empty set that's bounded from above by some value that's not in the set, in a certain kind of topological space, you can always find a sequence of values in the set that increases to this upper bound.
More concisely: In a countably generated topological linear ordered space, given a non-empty, bounded above, and non-containing set, there exists a strictly increasing sequence of elements from the set that converges to the upper bound.
|
IsLUB.mem_upperBounds_of_tendsto
theorem IsLUB.mem_upperBounds_of_tendsto :
∀ {α : Type u_1} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTopology α]
[inst_3 : Preorder γ] [inst_4 : TopologicalSpace γ] [inst_5 : OrderClosedTopology γ] {f : α → γ} {s : Set α}
{a : α} {b : γ},
MonotoneOn f s → IsLUB s a → Filter.Tendsto f (nhdsWithin a s) (nhds b) → b ∈ upperBounds (f '' s)
This theorem states that for a given set `s` of elements of type `α` and a function `f` from `α` to `γ`, if `f` is monotone on `s` and `a` is a least upper bound of `s`, then if the limit of `f` as elements approach `a` within `s` is `b`, then `b` belongs to the set of upper bounds of the image of `s` under `f`. In other words, if `f` is increasing over a set and we find its limit at a point which is a least upper bound for that set, then the limit value is an upper bound for the set of output values of `f`. This guarantee is given under certain conditions for the types `α` and `γ` - they must both be equipped with a topology, `α` must be a linear order with an order topology and `γ` must be a preorder with a closed order topology.
More concisely: If `f` is a monotone function from a non-empty, bounded above set `s` in a linearly ordered topological space `α` with a least upper bound `a`, and `b` is the limit of `f` as elements approach `a` in `s`, then `b` is an upper bound for the image of `s` under `f` in the preordered topological space `γ`.
|