IsCompact.exists_isMaxOn
theorem IsCompact.exists_isMaxOn :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
[inst_3 : ClosedIciTopology α] {s : Set β},
IsCompact s → s.Nonempty → ∀ {f : β → α}, ContinuousOn f s → ∃ x ∈ s, IsMaxOn f s x
This theorem is known as the "Extreme Value Theorem". It states that if we have a continuous function `f` from a compact, nonempty set `s` in a topological space, to a set in a linearly ordered topological space with a closed interval topology, then there exists an element `x` in `s` such that `f` attains its maximum at `x` for all elements in `s`. In other words, for a given continuous function on a compact, nonempty set, there will always be a point in the set where the function reaches its maximum value.
More concisely: If `f` is a continuous function on the compact, nonempty set `s` in a linearly ordered topological space with a closed interval topology, then there exists an element `x` in `s` such that for all `y` in `s`, `f(x)` is greater than or equal to `f(y)`.
|
Continuous.exists_forall_le'
theorem Continuous.exists_forall_le' :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
[inst_3 : ClosedIicTopology α] {f : β → α},
Continuous f → ∀ (x₀ : β), (∀ᶠ (x : β) in Filter.cocompact β, f x₀ ≤ f x) → ∃ x, ∀ (y : β), f x ≤ f y
The theorem, often known as the **Extreme Value Theorem**, states that if we have a continuous function `f` from a topological space `β` to a linearly ordered topological space `α` equipped with the closed lower interval topology, then if for some `x₀` in `β`, `f(x₀)` is less than or equal to `f(x)` for all `x` outside of compact sets in `β`, then there exists an `x` in `β` such that `f(x)` is less than or equal to `f(y)` for all `y` in `β`. In other words, a continuous function on a space like this always attains a global minimum if it stays larger than some value outside compact subsets.
More concisely: If a continuous function from a topological space to a linearly ordered topological space, with the domain restricted to compact sets, attains a minimum value at every compact subset, then the function attains a global minimum in the domain.
|
CompactIccSpace.isCompact_Icc
theorem CompactIccSpace.isCompact_Icc :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] [self : CompactIccSpace α] {a b : α},
IsCompact (Set.Icc a b)
The theorem `CompactIccSpace.isCompact_Icc` asserts that for any type `α` which is equipped with a topological space structure, a preorder structure, and for which `CompactIccSpace α` holds, for any two elements `a` and `b` of this type `α`, the left-closed right-closed interval `Set.Icc a b` is a compact set. In other words, for any nontrivial filter that contains this interval, there exists a point within the interval such that every set of this filter intersects every neighborhood of the point.
More concisely: For any type `α` with a topological space, preorder structure, and `CompactIccSpace α` property, the interval `Icc a b` of any two elements `a` and `b` is compact.
|
Continuous.bddAbove_range_of_hasCompactSupport
theorem Continuous.bddAbove_range_of_hasCompactSupport :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
[inst_3 : ClosedIciTopology α] [inst_4 : Zero α] {f : β → α},
Continuous f → HasCompactSupport f → BddAbove (Set.range f)
The theorem `Continuous.bddAbove_range_of_hasCompactSupport` states that for any continuous function `f` from a type `β` to a type `α`, if `f` has compact support (meaning the closure of the support of `f` is compact), then the range of `f` is bounded above. Here, `α` is a linearly ordered topological space with the topology induced by the order relation and `β` is a topological space. Being bounded above means there exists an upper bound for the set of all possible outputs of `f`. Essentially, this theorem says that for a continuous function with compact support, there is an upper limit to the values it can output.
More concisely: For any continuous function from a topological space to a linearly ordered topological space with compact support, its range is bounded above.
|
IsCompact.exists_isLeast
theorem IsCompact.exists_isLeast :
∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : ClosedIicTopology α] {s : Set α},
IsCompact s → s.Nonempty → ∃ x, IsLeast s x
This theorem states that for any set `s` of a given type `α`, where `α` has a linear order, topological space, and closed lower semi-continuous topology, if the set `s` is compact and nonempty, then there exists an element `x` in `s` that is the least element of the set `s`. In other words, any compact and nonempty set in such a space will always have a minimum element.
More concisely: If `α` is a type with a linear order, topology, and closed lower semi-continuous topology, then any compact and nonempty subset of `α` has a least element.
|
ContinuousOn.exists_forall_ge'
theorem ContinuousOn.exists_forall_ge' :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
[inst_3 : ClosedIciTopology α] {s : Set β} {f : β → α},
ContinuousOn f s →
IsClosed s →
∀ {x₀ : β},
x₀ ∈ s →
(∀ᶠ (x : β) in Filter.cocompact β ⊓ Filter.principal s, f x ≤ f x₀) → ∃ x ∈ s, ∀ y ∈ s, f y ≤ f x
The **extreme value theorem** states that if a function `f` from a topological space `β` to a linearly ordered topological space `α` is continuous on a closed set `s`, and it is smaller than or equal to a chosen value in its image except possibly on compact subsets of `β`, then it attains a maximum value on this set `s`. In other words, there exists an element in `s` where `f` reaches its maximum value when compared to its values at all other points in `s`. This theorem asserts the existence of maximum values for continuous functions on closed sets, under certain conditions about their behaviour near compact sets.
More concisely: If a continuous function on a closed set of a topological space attains a minimum value or is bounded below on compact subsets, then it reaches its maximum value on the set.
|
IsCompact.bddAbove_image
theorem IsCompact.bddAbove_image :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
[inst_3 : ClosedIciTopology α] [inst_4 : Nonempty α] {f : β → α} {K : Set β},
IsCompact K → ContinuousOn f K → BddAbove (f '' K)
The theorem "IsCompact.bddAbove_image" states that if we have a function `f` from a type `β` to a type `α`, where `α` is a linearly ordered set equipped with a topology that makes all intervals of the form "[x, +∞)" closed (ClosedIciTopology) and `β` is a topological space, and we have a non-empty set `K` in `β` which is compact, then if the function `f` is continuous on `K`, the image of `K` under `f` is bounded above, meaning there exists some element in `α` which is greater or equal to all elements in the image of `K` under `f`. In mathematical terms, for a continuous function `f` on a compact set `K`, there exists a value `M` such that `f(x) ≤ M` for all `x` in `K`.
More concisely: If `f` is a continuous function from the compact set `K` in a linearly ordered topological space `β`, then the image of `K` under `f` has a supremum in `α`.
|
IsCompact.bddBelow_image
theorem IsCompact.bddBelow_image :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
[inst_3 : ClosedIicTopology α] [inst_4 : Nonempty α] {f : β → α} {K : Set β},
IsCompact K → ContinuousOn f K → BddBelow (f '' K)
The theorem `IsCompact.bddBelow_image` states that for any linearly ordered topological space `α` and any topological space `β`, if `K` is a compact set in `β` and `f` is a function from `β` to `α` that is continuous on `K`, then the image of `K` under `f` is bounded below. In other words, there exists a lower bound for the set of all outputs from `f` when the inputs are taken from the compact set `K`.
More concisely: If `K` is a compact set in a topological space `β`, and `f` is a continuous function from `β` to a linearly ordered topological space `α`, then the image of `K` under `f` has a lowest element in `α`.
|
Continuous.exists_forall_ge
theorem Continuous.exists_forall_ge :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
[inst_3 : ClosedIciTopology α] [inst_4 : Nonempty β] {f : β → α},
Continuous f → Filter.Tendsto f (Filter.cocompact β) Filter.atBot → ∃ x, ∀ (y : β), f y ≤ f x
This is the statement of the **Extreme Value Theorem**: For any continuous function `f` from a non-empty topological space `β` to a linearly ordered topological space `α` with a closed interval topology, if `f` tends towards negative infinity outside of compact sets of `β`, then there exists a point `x` in `β` such that for all `y` in `β`, `f(y)` is less than or equal to `f(x)`. In other words, the function `f` has a global maximum.
More concisely: If a continuous function from a non-empty topological space to a linearly ordered topological space with a closed interval topology tends towards negative infinity outside of compact sets, then it attains a global maximum in the space.
|
Continuous.exists_forall_ge_of_hasCompactSupport
theorem Continuous.exists_forall_ge_of_hasCompactSupport :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
[inst_3 : ClosedIciTopology α] [inst_4 : Nonempty β] [inst_5 : Zero α] {f : β → α},
Continuous f → HasCompactSupport f → ∃ x, ∀ (y : β), f y ≤ f x
This theorem states that for any continuous function `f` from a non-empty type `β` to a type `α`, if `f` has compact support (meaning the closure of the set of points where `f` is non-zero is compact), then there exists a point `x` in `β` such that the function value `f(x)` is greater than or equal to the function value at any other point `y` in `β`. This implies that a continuous function with compact support has a global maximum. Here, `α` is a linearly ordered topological space with a topology that is closed on intervals of the form `[a, ∞)`, and `β` is a topological space.
More concisely: A continuous function from a non-empty compactly supported topological space to a linearly ordered topological space with the property that intervals of the form [a, ∞) are closed, has a global maximum.
|
Continuous.bddBelow_range_of_hasCompactMulSupport
theorem Continuous.bddBelow_range_of_hasCompactMulSupport :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
[inst_3 : ClosedIicTopology α] [inst_4 : One α] {f : β → α},
Continuous f → HasCompactMulSupport f → BddBelow (Set.range f)
The theorem states that for any continuous function `f` mapping from a type `β` to a type `α`, where `α` has a linear order, a topological space structure, and the `ClosedIicTopology` topology (where closed intervals of the form `(-∞, b]` are generated), and `β` has a topological space structure, if `f` has compact multiplicative support (i.e., the closure of the multiplicative support of `f` is compact), then the range of `f` is bounded below. In other words, there exists some value `a` such that for all `x` in the range of `f`, `a ≤ x`. This theorem essentially establishes a link between the compactness property of the support of a function and the boundedness of its range.
More concisely: If `f` is a continuous function from a compactly supported, topological space `β` to a linearly ordered and topologized type `α` with the `ClosedIicTopology`, then the image of `f` has a lowest element.
|
Continuous.exists_forall_le_of_hasCompactSupport
theorem Continuous.exists_forall_le_of_hasCompactSupport :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
[inst_3 : ClosedIicTopology α] [inst_4 : Nonempty β] [inst_5 : Zero α] {f : β → α},
Continuous f → HasCompactSupport f → ∃ x, ∀ (y : β), f x ≤ f y
This theorem states that if a function `f` from an arbitrary type `β` to a type `α` has certain properties, then it has a global minimum. More specifically, if `f` is a continuous function and has compact support (meaning that the closure of the set of all points where `f` is not zero is a compact set), then there exists an element `x` in `β` such that `f(x)` is less than or equal to `f(y)` for every other `y` in `β`.
Here, `α` is a type with a linear order, a topology, a closed lower interval topology, and a zero element, and `β` is a type with a topology and at least one element. The topology on `α` is such that the set of all elements less than or equal to a given one is closed. This theorem basically asserts the existence of a global minimum for continuous functions with compact support.
More concisely: If `f` is a continuous function from a compact topological space `β` to a totally ordered and topologized type `α` with compact support, then `f` attains a global minimum.
|
Continuous.exists_forall_le_of_hasCompactMulSupport
theorem Continuous.exists_forall_le_of_hasCompactMulSupport :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
[inst_3 : ClosedIicTopology α] [inst_4 : Nonempty β] [inst_5 : One α] {f : β → α},
Continuous f → HasCompactMulSupport f → ∃ x, ∀ (y : β), f x ≤ f y
The theorem states that for any type `α` with a linear order and a topological space structure that is also a closed interval and nonempty, and any type `β` with a topological space structure, if `f` is a continuous function from `β` to `α` that has compact multiplicative support, then there exists a global minimum of `f`. In other words, there exists an element `x` in `β` such that `f(x)` is less than or equal to `f(y)` for all `y` in `β`. The compact multiplicative support property of `f` means that the closure of the set of points where `f` is different from `1` is a compact set.
More concisely: If `α` is a type with a linear order and a topological space structure as a closed interval and nonempty set, and `β` is any type with a topological space structure, then a continuous function `f` from `β` to `α` with compact multiplicative support has a global minimum in `β`.
|
atTop_le_cocompact
theorem atTop_le_cocompact :
∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : NoMaxOrder α]
[inst_3 : ClosedIciTopology α], Filter.atTop ≤ Filter.cocompact α
The theorem `atTop_le_cocompact` states that for any type `α`, which has a linear order, a topological space structure, is without a maximum element (`NoMaxOrder α`), and such that the topology is closed for the set of all elements greater than or equal to a given one (`ClosedIciTopology α`), the filter representing the limit towards positive infinity (`Filter.atTop`) is smaller than or equal to the filter generated by the complements of compact sets (`Filter.cocompact α`) in the order of filters. This essentially means that every neighborhood of infinity (every set that contains all sufficiently large elements) also contains the complement of some compact set.
More concisely: For any type `α` with a linear order, without a maximum element, and a closed order topology, the filter of elements greater than any given one is contained in the filter generated by the complements of compact sets.
|
Continuous.exists_forall_le
theorem Continuous.exists_forall_le :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
[inst_3 : ClosedIicTopology α] [inst_4 : Nonempty β] {f : β → α},
Continuous f → Filter.Tendsto f (Filter.cocompact β) Filter.atTop → ∃ x, ∀ (y : β), f x ≤ f y
The **extreme value theorem** states that for any continuous function `f` from a nonempty topological space `β` to a linearly ordered topological space `α` with the order topology, if `f` tends to infinity away from compact sets of `β`, then there exists an `x` in `β` such that `f(x)` is less than or equal to `f(y)` for all `y` in `β`. In other words, `f` has a global minimum at `x`.
More concisely: If a continuous function from a nonempty topological space to a linearly ordered topological space with the order topology tends to infinity only on compact sets, then it attains a global minimum in the space.
|
IsCompact.sInf_mem
theorem IsCompact.sInf_mem :
∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : ClosedIicTopology α] {s : Set α}, IsCompact s → s.Nonempty → sInf s ∈ s
This theorem, `IsCompact.sInf_mem`, states that for any type `α` that has a conditionally complete linear order and a topological structure with the topology being the closed interval from negative infinity to a given number (closed on the right), given a set `s` of this type `α`, if `s` is compact (in the topological sense) and nonempty, then the infimum (greatest lower bound) of the set `s` is an element of the set `s`. In layman's terms, for certain types of ordered sets with suitable topology, if the set is compact and not empty, the smallest element in the set is indeed part of the set.
More concisely: If `α` is a type with a conditionally complete linear order and a topology as described, and `s` is a compact, nonempty subset of `α`, then the infimum of `s` belongs to `s`.
|
IsCompact.exists_forall_le
theorem IsCompact.exists_forall_le :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
[inst_3 : ClosedIicTopology α] {s : Set β},
IsCompact s → s.Nonempty → ∀ {f : β → α}, ContinuousOn f s → ∃ x ∈ s, ∀ y ∈ s, f x ≤ f y
The **extreme value theorem** states that, for any given continuous function `f` mapping from a compact set `s` in a topological space to a linearly ordered topological space, there always exists a point `x` in `s` such that the value of `f` at `x` is less than or equal to the value of `f` at any other point in `s`. In other words, a continuous function always attains its minimum value at some point in a compact set. This theorem assumes the set `s` is non-empty and the function `f` is continuous on this set.
More concisely: A continuous function on a compact set attains its minimum value.
|
IsCompact.bddBelow
theorem IsCompact.bddBelow :
∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : ClosedIicTopology α]
[inst_3 : Nonempty α] {s : Set α}, IsCompact s → BddBelow s
The theorem `IsCompact.bddBelow` states that for any type `α` that has a linear ordering, a topology, a closed lower half-space topology, and is non-empty, any compact set `s` of this type is bounded below. In other words, if `s` is a compact set in a topological space that also has a linear order and a closed interval topology, then there exists a lower bound for `s`. This is a property of compact sets in the context of topology combined with order theory.
More concisely: In a non-empty type with a linear ordering, a topology, and a closed lower half-space topology, every compact set has a lower bound.
|
ContinuousOn.exists_isMaxOn'
theorem ContinuousOn.exists_isMaxOn' :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
[inst_3 : ClosedIciTopology α] {s : Set β} {f : β → α},
ContinuousOn f s →
IsClosed s →
∀ {x₀ : β},
x₀ ∈ s → (∀ᶠ (x : β) in Filter.cocompact β ⊓ Filter.principal s, f x ≤ f x₀) → ∃ x ∈ s, IsMaxOn f s x
This theorem, known as the **Extreme Value Theorem**, states that for any function `f` from a set `β` to a linearly ordered set `α`, given that `f` is continuous on a closed subset `s` of `β` and that for any element `x₀` in `s`, `f`'s value at `x₀` is greater than its value at almost all points of `β` not in compact subsets and in `s`, there exists an element in `s` at which `f` attains its maximum. The conditions on `f` and `s` ensure that `f` behaves well within `s` and that `s` is a well-behaved topological space. In mathematical terms, it says that if a function is continuous on a closed set and it is smaller than a value in its image away from compact sets, then it has a maximum on this set.
More concisely: If a continuous function on a closed set attains its minimum value at all but a compact subset's worth of points, then it has a maximum value within that set.
|
Continuous.bddBelow_range_of_hasCompactSupport
theorem Continuous.bddBelow_range_of_hasCompactSupport :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
[inst_3 : ClosedIicTopology α] [inst_4 : Zero α] {f : β → α},
Continuous f → HasCompactSupport f → BddBelow (Set.range f)
This theorem states that for any continuous function `f` from a topological space `β` to a linearly ordered topological space `α` that has a compact support, the range of `f` is bounded below. Here, "compact support" means that the closure of the set of points where `f` is non-zero is compact, "continuous" refers to the standard notion of continuity in topology, and "bounded below" means that there exists a lower bound for the set of all function values.
More concisely: For any continuous function $f$ from a topological space $\beta$ to a linearly ordered topological space $\alpha$ with compact support, the range of $f$ has a lowest element.
|
ContinuousOn.exists_isMinOn'
theorem ContinuousOn.exists_isMinOn' :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
[inst_3 : ClosedIicTopology α] {s : Set β} {f : β → α},
ContinuousOn f s →
IsClosed s →
∀ {x₀ : β},
x₀ ∈ s → (∀ᶠ (x : β) in Filter.cocompact β ⊓ Filter.principal s, f x₀ ≤ f x) → ∃ x ∈ s, IsMinOn f s x
The Extreme Value Theorem states the following: Given a function 'f' from some type β to linear ordered type α, if 'f' is continuous on a closed set 's' and for some 'x₀' in 's', 'f' of 'x₀' is less than or equal to 'f' of 'x' for all 'x' in the intersection of the filter generated by complements to compact sets and the principal filter of 's', then there exists some 'x' in 's' such that 'f' attains its minimum at 'x' on the set 's'. Here, the continuity of 'f' on 's' means that 'f' is continuous at every point in 's', and a set being closed is defined in the context of a topological space.
More concisely: If a continuous function on a closed set attains its minimum value at a point in the set for all sets in the filter of complements to compact sets and the principal filter of the set, then there exists a minimum point in the set.
|
ContinuousOn.exists_forall_le'
theorem ContinuousOn.exists_forall_le' :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
[inst_3 : ClosedIicTopology α] {s : Set β} {f : β → α},
ContinuousOn f s →
IsClosed s →
∀ {x₀ : β},
x₀ ∈ s →
(∀ᶠ (x : β) in Filter.cocompact β ⊓ Filter.principal s, f x₀ ≤ f x) → ∃ x ∈ s, ∀ y ∈ s, f x ≤ f y
The **extreme value theorem** states that for any function `f` from a set `β` to a set `α`, where `α` has a linear order and `β` has a topological structure, if `f` is continuous on a closed subset `s` of `β` and if for some point `x₀` in `s`, `f` is greater than or equal to its value everywhere in `s` except possibly on compact subsets, then there exists a point in `s` where `f` attains its minimum over `s`. In other words, this theorem asserts that under the given conditions, the function `f` has a minimum value in the set `s`.
More concisely: If a continuous function `f` on a closed subset `s` of a topological space `β`, where `α` (range of `f`) has a linear order, has a minimum value in `α` and is greater than or equal to that value on all compact subsets of `s`, then there exists a point in `s` where `f` attains that minimum value.
|
ContinuousOn.image_Icc
theorem ContinuousOn.image_Icc :
∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] [inst_3 : TopologicalSpace β] [inst_4 : DenselyOrdered α]
[inst_5 : ConditionallyCompleteLinearOrder β] [inst_6 : OrderTopology β] {f : α → β} {a b : α},
a ≤ b →
ContinuousOn f (Set.Icc a b) → f '' Set.Icc a b = Set.Icc (sInf (f '' Set.Icc a b)) (sSup (f '' Set.Icc a b))
This theorem states that for any two types `α` and `β`, provided that `α` and `β` are both conditionally complete linear ordered spaces with a topological structure and `α` is densely ordered, and given a function `f` from `α` to `β` and two elements `a` and `b` in `α` such that `a` is less than or equal to `b`, if `f` is continuous on the closed interval `[a, b]`, then the image of the interval `[a, b]` under `f` is the closed interval from the greatest lower bound of the image to the least upper bound of the image, denoted as `[sInf (f '' Set.Icc a b), sSup (f '' Set.Icc a b)]`.
More concisely: Given two conditionally complete, topological linear ordered spaces `α` and `β`, where `α` is densely ordered, and a continuous function `f` from `α` to `β` such that `a ≤ b` are elements of `α`, then the image of the closed interval `[a, b]` under `f` is the closed interval `[inf(f(a:α):β), sup(f(b:α):β)]`.
|
IsCompact.exists_forall_ge
theorem IsCompact.exists_forall_ge :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
[inst_3 : ClosedIciTopology α] {s : Set β},
IsCompact s → s.Nonempty → ∀ {f : β → α}, ContinuousOn f s → ∃ x ∈ s, ∀ y ∈ s, f y ≤ f x
The Extreme Value Theorem states that for a continuous function defined on a compact and nonempty set, there exists a point within the set at which the function attains its maximum value. In other words, given a compact and nonempty set `s` in some topological space, and a continuous function `f` acting on `s`, there exists a point `x` in `s` such that for all other points `y` in `s`, the value of the function `f` at `y` is less than or equal to the value of `f` at `x`. This theorem is foundational in real analysis and optimization, where it is used to guarantee the existence of maximum and minimum values of functions under certain conditions.
More concisely: For a continuous function defined on a compact and nonempty set, there exists a point in the set where the function reaches its maximum value.
|
cocompact_eq_atBot_atTop
theorem cocompact_eq_atBot_atTop :
∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : NoMaxOrder α]
[inst_3 : NoMinOrder α] [inst_4 : OrderClosedTopology α] [inst_5 : CompactIccSpace α],
Filter.cocompact α = Filter.atBot ⊔ Filter.atTop
The theorem `cocompact_eq_atBot_atTop` states that for any type `α` that has a linear order, a topology, and no maximum or minimum elements (i.e., it extends indefinitely in both positive and negative directions), with the topology being closed with respect to the order and the space of all closed intervals being compact, the filter generated by the complements of compact sets (i.e., the cocompact filter) is equal to the join of the filters representing the limits to negative infinity (`atBot`) and positive infinity (`atTop`). In simpler terms, in such a set, the notion of "going to infinity in either direction" is equivalent to "running out of compact sets".
More concisely: For a type `α` with a linear order, topology, no maximum or minimum elements, a compact space of intervals, and a topology closed with respect to the order, the cocompact filter is equal to the join of filters `atBot` and `atTop`.
|
Continuous.exists_forall_ge'
theorem Continuous.exists_forall_ge' :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
[inst_3 : ClosedIciTopology α] {f : β → α},
Continuous f → ∀ (x₀ : β), (∀ᶠ (x : β) in Filter.cocompact β, f x ≤ f x₀) → ∃ x, ∀ (y : β), f y ≤ f x
This Lean theorem states the **extreme value theorem**, which is an important result in calculus and real analysis. In more detail, the theorem says: For any types `α` and `β`, where `α` has a linear order and both `α` and `β` are topological spaces (with `α` having a topology that is closed on the right), if you have a continuous function `f` from `β` to `α`, and for some `x₀` in `β` the function `f` is smaller or equal to `f(x₀)` away from compact sets in `β`, then there exists a point in `β` at which `f` attains its global maximum, i.e., `f` is smaller or equal to `f` at that point for all inputs in `β`.
More concisely: If `α` is a type with a linear order and a topology closed on the right, `β` is a topological space, and `f: β → α` is a continuous function such that `f(x) ≤ f(x₀)` for all `x ≠ x₀` in some `x₀` in `β`, then `f` attains its global maximum at some point in `β`.
|
atBot_le_cocompact
theorem atBot_le_cocompact :
∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : NoMinOrder α]
[inst_3 : ClosedIicTopology α], Filter.atBot ≤ Filter.cocompact α
The theorem `atBot_le_cocompact` states that, for any type `α` equipped with a linear order, a topological space structure, an ordering without a minimal element (`NoMinOrder`), and a topology where the closed interval `(-∞, a]` is closed for each `a` (`ClosedIicTopology`), the filter representing the limit towards negative infinity (`Filter.atBot`) is less than or equal to the filter generated by the complements of compact sets (`Filter.cocompact`). In simpler terms, any sequence in `α` that tends to negative infinity is eventually in the complement of any given compact set.
More concisely: For any type `α` with a linear order, NoMinOrder, ClosedIicTopology, and for filters `Filter.atBot` and `Filter.cocompact`, `Filter.atBot ≤ Filter.cocompact`. That is, any sequence in `α` tending to negative infinity is eventually contained in the complement of every compact set.
|
Continuous.exists_forall_ge_of_hasCompactMulSupport
theorem Continuous.exists_forall_ge_of_hasCompactMulSupport :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
[inst_3 : ClosedIciTopology α] [inst_4 : Nonempty β] [inst_5 : One α] {f : β → α},
Continuous f → HasCompactMulSupport f → ∃ x, ∀ (y : β), f y ≤ f x
The theorem `Continuous.exists_forall_ge_of_hasCompactMulSupport` states that for any continuous function `f` from a non-empty space `β` to a linear-ordered space `α`, if `f` has compact multiplicative support, then there exists a point `x` in `β` such that `f(x)` is greater than or equal to `f(y)` for all `y` in `β`. In other words, a continuous function with compact support has a global maximum.
More concisely: A continuous function from a non-empty space to a linear-ordered space with compact multiplicative support has a global maximum in its domain.
|
IsCompact.bddAbove
theorem IsCompact.bddAbove :
∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : ClosedIciTopology α]
[inst_3 : Nonempty α] {s : Set α}, IsCompact s → BddAbove s
This theorem states that a compact set is always bounded above. More specifically, for any set `s` in a linearly ordered, topologically structured space (with a topology that contains the topology induced by the given linear order), if the set `s` is compact, then there exists an upper bound for `s`. This upper bound need not be an element of the set, but is an element such that all elements of `s` are less than or equal to this upper bound. The space is also assumed to be nonempty, which means it contains at least one element.
More concisely: In a nonempty, linearly ordered and topologically structured space, every compact set has an upper bound.
|
isCompact_uIcc
theorem isCompact_uIcc :
∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : CompactIccSpace α] {a b : α},
IsCompact (Set.uIcc a b)
This theorem states that an unordered closed interval is compact. In other words, for any type `α` that has a linear order, a topology, and the closed interval `[a, b]` is a compact subset, the unordered interval between any two elements `a` and `b` of `α` is also a compact set. In formal terms, if `f` is any filter on `α` that is not the empty set and contains the unordered interval, then there is an element `x` in the unordered interval such that every set in the filter `f` intersects every neighborhood of `x`.
More concisely: For any type `α` with a linear order and topology, every unordered closed interval is compact. That is, given a filter `f` on `α` that contains an unordered interval, there exists an element in the interval belonging to every set in the filter that intersects every neighborhood of that element.
|
IsCompact.exists_isMinOn
theorem IsCompact.exists_isMinOn :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
[inst_3 : ClosedIicTopology α] {s : Set β},
IsCompact s → s.Nonempty → ∀ {f : β → α}, ContinuousOn f s → ∃ x ∈ s, IsMinOn f s x
The **extreme value theorem** states that for any given continuous function that maps from a compact set in a topological space to a linearly ordered set with an order-closed lower set topology, there exists a point in the compact set where the function reaches its minimum value. In other words, a continuous function will always have a minimum value on a compact set. Moreover, if the set is non-empty, then this minimum point is guaranteed to be within the set itself.
More concisely: A continuous function on a compact set in a topological space attains its minimum value in the set.
|
Continuous.bddAbove_range_of_hasCompactMulSupport
theorem Continuous.bddAbove_range_of_hasCompactMulSupport :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
[inst_3 : ClosedIciTopology α] [inst_4 : One α] {f : β → α},
Continuous f → HasCompactMulSupport f → BddAbove (Set.range f)
The theorem `Continuous.bddAbove_range_of_hasCompactMulSupport` states that, for any types `α` and `β` where `α` is a linearly ordered, topological space with a closed half-space topology, and `β` is a topological space, for any function `f` from `β` to `α` that is continuous and has compact multiplicative support, the range of `f` is bounded above. In simpler terms, it says that the set of values a continuous function takes, when the function is equal to `1` outside a compact set, always has an upper bound.
More concisely: If `f` is a continuous function from a topological space `β` to a linearly ordered, topological space `α` with a closed half-space topology, and `f` has compact multiplicative support, then the range of `f` is bounded above.
|