IsPreconnected.mem_intervals
theorem IsPreconnected.mem_intervals :
∀ {α : Type u} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
{s : Set α},
IsPreconnected s →
s ∈
{Set.Icc (sInf s) (sSup s), Set.Ico (sInf s) (sSup s), Set.Ioc (sInf s) (sSup s), Set.Ioo (sInf s) (sSup s),
Set.Ici (sInf s), Set.Ioi (sInf s), Set.Iic (sSup s), Set.Iio (sSup s), Set.univ, ∅}
This theorem states that in a conditionally complete linear order with a given topology and an order topology, if a set is preconnected, then it must be one of the following types of intervals: a closed interval from the infimum to the supremum of the set (denoted as `[Inf s, Sup s]`), a left-closed right-open interval from the infimum to the supremum (denoted as `[Inf s, Sup s)`), a left-open right-closed interval (denoted as `(Inf s, Sup s]`), an open interval (denoted as `(Inf s, Sup s)`), a left-closed right-infinite interval (denoted as `[Inf s, +∞)`), a left-open right-infinite interval (denoted as `(Inf s, +∞)`), a left-infinite right-closed interval (denoted as `(-∞, Sup s]`), a left-infinite right-open interval (denoted as `(-∞, Sup s)`), the universal set (denoted as `(-∞, +∞)`, or `Set.univ`), or the empty set (`∅`). The converse statement, however, requires the additional condition that the set needs to be densely ordered.
More concisely: In a conditionally complete linear order with a given topology and an order topology, a preconnected set is an interval of the form [Inf s, Sup s], [Inf s, Sup s), (Inf s, Sup s], (Inf s, Sup s), [Inf s, +∞), (Inf s, +∞), (-∞, Sup s], (-∞, Sup s), (-∞, +∞), or ∅, where Inf s and Sup s denote the infimum and supremum of the set, respectively, and the set is either densely ordered if the converse statement applies.
|
Continuous.strictMono_of_inj_boundedOrder
theorem Continuous.strictMono_of_inj_boundedOrder :
∀ {α : Type u} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ]
[inst_6 : OrderClosedTopology δ] [inst_7 : BoundedOrder α] {f : α → δ},
Continuous f → f ⊥ ≤ f ⊤ → Function.Injective f → StrictMono f
The theorem `Continuous.strictMono_of_inj_boundedOrder` states that for any types `α` and `δ`, where `α` is a conditionally complete linear order with a topology, order topology, and densely ordered, and `δ` is a linear order with a topology and order-closed topology, and `α` has a bounded order, given a function `f` from `α` to `δ`, if the function `f` is continuous and the image of the least element of `α` under `f` is less than or equal to the image of the greatest element of `α` under `f`, and `f` is injective, then `f` is strictly monotonic. In other words, a continuous and injective function from a bounded, densely ordered space to a linearly ordered space is strictly increasing provided it preserves the order of the bounding elements.
More concisely: A continuous, injective function from a bounded, densely ordered space to a linearly ordered space with order-closed topology is strictly increasing if it maps the least element to less than or equal to the image of the greatest element.
|
setOf_isPreconnected_eq_of_ordered
theorem setOf_isPreconnected_eq_of_ordered :
∀ {α : Type u} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α],
{s | IsPreconnected s} =
Set.range (Function.uncurry Set.Icc) ∪ Set.range (Function.uncurry Set.Ico) ∪
Set.range (Function.uncurry Set.Ioc) ∪
Set.range (Function.uncurry Set.Ioo) ∪
(Set.range Set.Ici ∪ Set.range Set.Ioi ∪ Set.range Set.Iic ∪ Set.range Set.Iio ∪ {Set.univ, ∅})
This theorem states that in the context of a dense conditionally complete linear order with a corresponding topological space and order topology, the set of preconnected sets is exactly equivalent to the set containing all possible intervals, which include closed intervals (`Icc`), half-open intervals (`Ico` and `Ioc`), open intervals (`Ioo`), right-infinite intervals (either open `Ioi` or closed `Ici`), left-infinite intervals (either open `Iio` or closed `Iic`), the entire set (`Set.univ`), or the empty set (`∅`). Even though the empty set could be represented as an interval where the infimum equals the supremum, it's included separately for better readability.
More concisely: In a dense, conditionally complete linear order, the preconnected sets are exactly the sets equivalent to the intervals (closed, half-open, open, left-infinite, right-infinite, entire, and empty).
|
IsConnected.Icc_subset
theorem IsConnected.Icc_subset :
∀ {α : Type v} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderClosedTopology α] {s : Set α},
IsConnected s → ∀ {a b : α}, a ∈ s → b ∈ s → Set.Icc a b ⊆ s
The theorem `IsConnected.Icc_subset` states that if we have a preconnected set `s` in a topological space `α`, which is also a linear order with an order-closed topology, and if this set contains the endpoints `a` and `b` of an interval (where `a` ≤ `x` ≤ `b` for all `x` in the interval), then the entire interval (inclusive of both endpoints `a` and `b`) is contained within the set `s`. In other words, if a preconnected set contains two points, it also contains the entire interval bounded by those two points.
More concisely: If `s` is a preconnected, order-closed subset of a linear order topology and contains the endpoints `a` and `b`, then `[a, b] ⊆ s`.
|
IsPreconnected.intermediate_value
theorem IsPreconnected.intermediate_value :
∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
[inst_3 : OrderClosedTopology α] {s : Set X},
IsPreconnected s → ∀ {a b : X}, a ∈ s → b ∈ s → ∀ {f : X → α}, ContinuousOn f s → Set.Icc (f a) (f b) ⊆ f '' s
This theorem is a statement of the Intermediate Value Theorem for continuous functions on connected sets in topology. In more detail, it says that for any type `X` with a topology, a linearly ordered type `α` also with a topology and an order-closed topology, and a set `s` of type `X` that is preconnected, for any two elements `a` and `b` in `s` and a function `f` from `X` to `α` that is continuous on `s`, the closed interval between `f(a)` and `f(b)` in `α` is a subset of the image of `f` applied to `s`. In simpler terms, if you have a continuous function on a connected set, then any value between the function values at two points in that set can be achieved by the function within that set.
More concisely: If `X` is a connected topological space, `α` is a linearly ordered and order-closed topological space, `s` is a preconnected subset of `X`, and `f` is a continuous function from `X` to `α`, then the image of `s` contains the closed interval between `f(a)` and `f(b)` for any `a, b` in `s`.
|
ContinuousOn.surjOn_of_tendsto'
theorem ContinuousOn.surjOn_of_tendsto' :
∀ {α : Type u} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ]
[inst_6 : OrderClosedTopology δ] {f : α → δ} {s : Set α} [inst_7 : s.OrdConnected],
s.Nonempty →
ContinuousOn f s →
Filter.Tendsto (fun x => f ↑x) Filter.atBot Filter.atTop →
Filter.Tendsto (fun x => f ↑x) Filter.atTop Filter.atBot → Set.SurjOn f s Set.univ
This theorem states that if a function `f` from a type `α` to `β` is continuous on a nonempty interval `s` and its restriction to `s` tends to infinity along the sequence approaching negative infinity (`Filter.atTop` along `Filter.atBot`) and tends to negative infinity along the sequence approaching infinity (`Filter.atBot` along `Filter.atTop`), then the restriction of `f` to `s` is surjective. In other words, for every point in the universe of `β`, there exists a point in `s` such that applying `f` to this point produces the point in `β`. The types `α` and `β` must be conditionally complete linear orders with topological structure, and `s` must be an ordered and connected subset of `α`. Also, the topology on `α` and `β` must be an order topology and order closed topology respectively, and `α` must be densely ordered.
More concisely: If `f` is a continuous function from a nonempty, ordered and connected subset `s` of a densely ordered, conditionally complete linear order `α` to another conditionally complete linear order `β` with order topology, such that `f` tends to infinity on both negative and positive sequences in `s`, then `f` is surjective on `s`.
|
intermediate_value_uIcc
theorem intermediate_value_uIcc :
∀ {α : Type u} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ]
[inst_6 : OrderClosedTopology δ] {a b : α} {f : α → δ},
ContinuousOn f (Set.uIcc a b) → Set.uIcc (f a) (f b) ⊆ f '' Set.uIcc a b
The Intermediate Value Theorem for continuous functions on closed intervals, unordered case, states that for any types `α` and `δ`, where `α` is a conditionally complete linear order, has a topological space structure, an order topology, and is densely ordered, and `δ` is a linear order with a topological space structure and order-closed topology, for any two elements `a` and `b` of `α` and a function `f` from `α` to `δ`, if the function `f` is continuous on the set of elements lying between `a` and `b` including `a` and `b`, then the set of elements in `δ` between `f(a)` and `f(b)` including `f(a)` and `f(b)` is a subset of the image of the aforementioned set under `f`. This theorem captures the intuition that a continuous function takes on every value between its minimum and maximum values on a closed interval.
More concisely: If `α` is a densely ordered, conditionally complete linear order with a topology making it a topological space, `δ` is a linearly ordered topological space with an order-closed topology, and `f` is a continuous function from `α` to `δ`, then the image of any closed interval `[a, b]` in `α` under `f` contains all elements of `δ` between `f(a)` and `f(b)`.
|
intermediate_value_univ₂
theorem intermediate_value_univ₂ :
∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
[inst_3 : OrderClosedTopology α] [inst_4 : PreconnectedSpace X] {a b : X} {f g : X → α},
Continuous f → Continuous g → f a ≤ g a → g b ≤ f b → ∃ x, f x = g x
This theorem is a version of the Intermediate Value Theorem for two functions. Specifically, it states that if `f` and `g` are two continuous functions on a preconnected topological space (a topological space that cannot be represented as the union of two disjoint nonempty open sets), and `f(a)` is less than or equal to `g(a)`, and `g(b)` is less than or equal to `f(b)`, then there exists some point `x` in the space such that `f(x)` equals `g(x)`. In simpler terms, if two continuous functions cross over each other at least once between any two points, then there must be a point where they are equal.
More concisely: If `f` and `g` are continuous functions on a connected topological space with `f(a) ≤ g(a)` and `g(b) ≤ f(b)`, then there exists an `x` in the space such that `f(x) = g(x)`.
|
Continuous.surjective'
theorem Continuous.surjective' :
∀ {α : Type u} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ]
[inst_6 : OrderClosedTopology δ] {f : α → δ},
Continuous f →
Filter.Tendsto f Filter.atBot Filter.atTop →
Filter.Tendsto f Filter.atTop Filter.atBot → Function.Surjective f
This theorem states that for any continuous function `f` mapping from an ordered and topological space `α` to an ordered and topological space `δ`, if the function tends to negative infinity (`Filter.atBot`) as the input approaches positive infinity (`Filter.atTop`), and tends to positive infinity (`Filter.atTop`) as the input approaches negative infinity (`Filter.atBot`), then the function `f` is surjective. In other words, for every value in the destination space `δ`, there exists a corresponding value in the source space `α` such that the function applied to this source value equals the target value. This is true in a conditionally complete linear order and densely ordered setting for `α`, and a linear and order-closed topology setting for `δ`.
More concisely: If a continuous function between ordered and topological spaces `α` and `δ`, where `α` is conditionally complete, densely ordered, and `δ` is linear and order-closed, maps `Filter.atBot` of `α` to `Filter.atTop` of `δ` and `Filter.atTop` of `α` to `Filter.atBot` of `δ`, then the function is surjective.
|
isPreconnected_iff_ordConnected
theorem isPreconnected_iff_ordConnected :
∀ {α : Type u} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] {s : Set α}, IsPreconnected s ↔ s.OrdConnected
The theorem `isPreconnected_iff_ordConnected` states that for a set `s` of a type `α`, under the conditions that `α` is a conditionally complete linear order, it has a topological space structure, an order topology and it's densely ordered, then `s` is preconnected if and only if `s` is order connected. In other words, in this mathematical context, a set is preconnected (there is no non-trivial open partition of the set) if and only if it is order connected (for any two points in the set, all the points between them are also in the set).
More concisely: In a densely ordered, conditionally complete linear order `α` with order topology, a set `s` is preconnected if and only if it is order connected.
|
isPreconnected_Ioc
theorem isPreconnected_Ioc :
∀ {α : Type u} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] {a b : α}, IsPreconnected (Set.Ioc a b)
The theorem `isPreconnected_Ioc` states that for any type `α` that has a conditionally complete linear order, a topological space structure, an order topology structure, and a densely ordered structure, and for any two elements `a` and `b` in this type `α`, the left-open right-closed interval from `a` to `b` (denoted as `(a, b]` in mathematical notation), is a preconnected set.
In simpler terms, this theorem says that in a properly ordered and topologically structured set, any interval that is open on the left and closed on the right is a preconnected set. A preconnected set is one where there is no non-trivial open partition, meaning we cannot divide it into two non-empty open sets that are disjoint and their union is the set itself.
More concisely: In a type equipped with a conditionally complete linear order, topological space structure, and densely ordered structure, every left-open right-closed interval is a preconnected set.
|
IsClosed.Icc_subset_of_forall_exists_gt
theorem IsClosed.Icc_subset_of_forall_exists_gt :
∀ {α : Type u} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
{a b : α} {s : Set α},
IsClosed (s ∩ Set.Icc a b) →
a ∈ s → (∀ x ∈ s ∩ Set.Ico a b, ∀ y ∈ Set.Ioi x, (s ∩ Set.Ioc x y).Nonempty) → Set.Icc a b ⊆ s
This theorem, known as the "continuous induction principle" for a closed interval, states that given a set `s` and two elements `a` and `b` such that `a` is in `s` and `s` intersects with the closed interval from `a` to `b` on a closed subset, if for any `x` such that `a ≤ x < y ≤ b` and `x` is in `s`, the set `s` intersects with the open-closed interval from `x` to `y` (i.e., `s ∩ (x, y]` is not empty), then the closed interval from `a` to `b` is a subset of `s`. Here, `α` is any type that has a conditionally complete linear order, a topological space, and an order topology.
More concisely: If a set `s` contains `a` and intersects the closed interval [`a`, `b`] on a closed subset, and for all `x` in the interval with `a ≤ x < b`, `s` intersects the open-closed interval `(x, b] non-empty, then `s` contains the closed interval [`a`, `b`].
|
Set.OrdConnected.isPreconnected
theorem Set.OrdConnected.isPreconnected :
∀ {α : Type u} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] {s : Set α}, s.OrdConnected → IsPreconnected s
This theorem states that for any type `α` that has the structure of both a conditionally complete linear order and a topological space with an order topology, and is densely ordered, if a set `s` of type `α` is order-connected (every interval [a, b] with a, b in the set lies within the set), then it is also preconnected.
In a preconnected set, there is no non-trivial open partition: for any two open sets `u` and `v`, if the set `s` is a subset of the union of `u` and `v`, and `s` intersects both `u` and `v`, then it must also intersect the intersection of `u` and `v`. This intersection is nonempty.
More concisely: In a densely ordered type `α` with both a conditional complete linear order and a topology, every order-connected subset is preconnected.
|
isPreconnected_Icc
theorem isPreconnected_Icc :
∀ {α : Type u} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] {a b : α}, IsPreconnected (Set.Icc a b)
This theorem states that for any type `α` that has a ConditionallyCompleteLinearOrder, a TopologicalSpace, an OrderTopology, and is DenselyOrdered, any closed interval `(Set.Icc a b)` is preconnected. In mathematical terms, it means that for any closed interval in a densely ordered conditionally complete linear order, there is no non-trivial open partition. Specifically, given any two open sets `u` and `v`, if the interval is a subset of the union `u ∪ v` and the interval intersects both `u` and `v`, then it must also intersect the intersection `u ∩ v`.
More concisely: In a densely ordered, conditionally complete linear order with a topology making it an order topology, every closed interval is preconnected, meaning that for any open sets `u` and `v` intersecting an interval, their intersection also intersects the interval.
|
IsConnected.Ioo_csInf_csSup_subset
theorem IsConnected.Ioo_csInf_csSup_subset :
∀ {α : Type u} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
{s : Set α}, IsConnected s → BddBelow s → BddAbove s → Set.Ioo (sInf s) (sSup s) ⊆ s
This theorem states that for any type `α` that is a conditionally complete linear order, which is equipped with a topological space structure and an order topology, if you have a set `s` of this type `α` that is connected, bounded below, and bounded above, then the open interval `(Inf s, Sup s)` is a subset of `s`. In other words, if you have a connected set `s` in a conditionally complete linear order that is bounded both above and below, all the elements between the infimum and supremum (not inclusive) of that set are also elements of the set.
More concisely: In a conditionally complete linear order with topology, if a connected, bounded below and bounded above subset `s` has infimum `Inf s` and supremum `Sup s`, then `(Inf s, Sup s) ⊆ s`.
|
setOf_isPreconnected_subset_of_ordered
theorem setOf_isPreconnected_subset_of_ordered :
∀ {α : Type u} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α],
{s | IsPreconnected s} ⊆
Set.range (Function.uncurry Set.Icc) ∪ Set.range (Function.uncurry Set.Ico) ∪
Set.range (Function.uncurry Set.Ioc) ∪
Set.range (Function.uncurry Set.Ioo) ∪
(Set.range Set.Ici ∪ Set.range Set.Ioi ∪ Set.range Set.Iic ∪ Set.range Set.Iio ∪ {Set.univ, ∅})
This theorem states that for any type 'α' that has a conditionally complete linear order, a topological space, and an order topology, the set of all preconnected sets is a subset of the union of the ranges of the functions that generate the intervals `Icc` (closed interval), `Ico` (left-closed right-open interval), `Ioc` (left-open right-closed interval), `Ioo` (open interval), `Ici` (left-closed right-infinite interval), `Ioi` (left-open right-infinite interval), `Iic` (left-infinite right-closed interval), `Iio` (left-infinite right-open interval), the universal set 'univ', and the empty set. In other words, every preconnected set can be represented as one of these types of intervals, or as the universal set, or the empty set. The reverse of this statement would require 'α' to be densely ordered. Although the empty set can be represented as an interval where both the lower and upper bounds are the infimum of 's', it is explicitly included in the list for the sake of readability.
More concisely: For any type 'α' with a conditionally complete linear order and an order topology, the preconnected sets form a subset of the universally quantified set of intervals and the empty set.
|
ContinuousOn.surjOn_of_tendsto
theorem ContinuousOn.surjOn_of_tendsto :
∀ {α : Type u} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ]
[inst_6 : OrderClosedTopology δ] {f : α → δ} {s : Set α} [inst_7 : s.OrdConnected],
s.Nonempty →
ContinuousOn f s →
Filter.Tendsto (fun x => f ↑x) Filter.atBot Filter.atBot →
Filter.Tendsto (fun x => f ↑x) Filter.atTop Filter.atTop → Set.SurjOn f s Set.univ
The theorem `ContinuousOn.surjOn_of_tendsto` states that if a function `f` from some type `α` to `δ`, where `α` and `δ` are equipped with appropriate topological and order structures, is continuous on a nonempty and connected interval `s`, and the restriction of `f` to `s` tends to negative infinity along the filter corresponding to `s` going to negative infinity (expressed as `Filter.Tendsto (fun x => f ↑x) Filter.atBot Filter.atBot`) and tends to positive infinity along the filter corresponding to `s` going to positive infinity (expressed as `Filter.Tendsto (fun x => f ↑x) Filter.atTop Filter.atTop`), then the function `f` is surjective when restricted to `s` (in other words, every element in the codomain can be obtained by applying `f` to some element in `s`). This surjectivity is formulated as `Set.SurjOn f s Set.univ`, which says that the image of `s` under `f` contains the entire set (universe) of type `δ`.
More concisely: If a continuous function from a nonempty, connected interval to a complete ordered topological space tends to negative infinity at one endpoint and positive infinity at the other, then it is surjective on that interval.
|
isPreconnected_Ico
theorem isPreconnected_Ico :
∀ {α : Type u} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] {a b : α}, IsPreconnected (Set.Ico a b)
This theorem states that for any type `α` which has a conditionally complete linear order, a topological space structure, an order topology and is densely ordered, the left-closed right-open interval from `a` to `b`, denoted as `Set.Ico a b`, is preconnected. In mathematical terms, it means that there is no non-trivial open partition for this interval. That is, for any open sets `u` and `v`, if the interval is a subset of the union of `u` and `v`, and there are points in the interval that belong to both `u` and `v`, then there must exist a point in the interval that belongs to the intersection of `u` and `v`.
More concisely: For any densely ordered type `α` with a conditionally complete linear order, topology, and order topology, the left-closed right-open interval `Set.Ico a b` is preconnected, meaning there is no open partition with no point in their intersection if the interval is a subset of their union and contains common points.
|
IsClosed.Icc_subset_of_forall_mem_nhdsWithin
theorem IsClosed.Icc_subset_of_forall_mem_nhdsWithin :
∀ {α : Type u} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] {a b : α} {s : Set α},
IsClosed (s ∩ Set.Icc a b) → a ∈ s → (∀ x ∈ s ∩ Set.Ico a b, s ∈ nhdsWithin x (Set.Ioi x)) → Set.Icc a b ⊆ s
This theorem, referred to as "continuous induction principle" for a closed interval, states that for a given type `α` that is a conditionally complete linear order with a topological space structure, order topology, and is densely ordered, if we have a set `s` and two elements `a` and `b` of type `α`, the following conditions imply that the closed interval `[a, b]` is a subset of `s`:
1) The intersection of set `s` and the closed interval `[a, b]` forms a closed set.
2) The element `a` is a member of the set `s`.
3) For any element `x` that belongs to the intersection of set `s` and the half-open interval `[a, b)`, set `s` includes an open neighborhood of `x` within the right-infinite open interval `(x, +∞)`.
In other words, if a set `s` intersects a closed interval at a closed subset, includes the lower bound of the interval, and for any point in the intersection of `s` and the left-closed right-open interval, `s` contains an open neighborhood within the rest of the number line beyond this point, then the entire closed interval is contained in set `s`.
More concisely: If a densely ordered, conditionally complete linear order `α` with a topology and a subset `s` satisfy the conditions that the intersection of `s` and the closed interval `[a, b]` is closed, `a` is in `s`, and for every `x` in the intersection of `s` and `[a, b)`, there exists an open neighborhood of `x` in `s` in the right-infinite open interval `(x, +∞)`, then the closed interval `[a, b]` is a subset of `s`.
|
ContinuousOn.surjOn_uIcc
theorem ContinuousOn.surjOn_uIcc :
∀ {α : Type u} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ]
[inst_6 : OrderClosedTopology δ] {s : Set α} [hs : s.OrdConnected] {f : α → δ},
ContinuousOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → Set.SurjOn f s (Set.uIcc (f a) (f b))
**Intermediate Value Theorem**: Given a function `f` from a type `α` to a type `δ`, where `α` is a densely ordered type equipped with a conditional complete linear order, topological space, order topology, and `δ` is a type with a linear order, topological space and order closed topology. If `f` is continuous on a set `s` in `α`, that is order-connected, and `a` and `b` are two points in this set `s`, then the function `f` maps the set `s` onto a superset of the interval between `f(a)` and `f(b)`, inclusive of `f(a)` and `f(b)`. This means that every value between `f(a)` and `f(b)` is the image of some point in `s` under `f`. This is the formalization of the classical intermediate value theorem from calculus in the context of general topological spaces.
More concisely: If a continuous function between a densely ordered, topological space with a complete order topology and a linearly ordered, topological space with a closure order topology maps an order-connected subset to an interval between its images of two points in the subset, then the image of the subset includes that interval.
|
IsPreconnected.intermediate_value₂
theorem IsPreconnected.intermediate_value₂ :
∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
[inst_3 : OrderClosedTopology α] {s : Set X},
IsPreconnected s →
∀ {a b : X},
a ∈ s →
b ∈ s → ∀ {f g : X → α}, ContinuousOn f s → ContinuousOn g s → f a ≤ g a → g b ≤ f b → ∃ x ∈ s, f x = g x
The theorem `IsPreconnected.intermediate_value₂` states that, given a preconnected set `s` in a topological space `X` with a linear ordering and a topological structure on a type `α` which is order-closed, if `f` and `g` are two functions that are continuous on `s` and for two points `a` and `b` in `s` where `f a` is less than or equal to `g a` and `g b` is less than or equal to `f b`, then there exists a point `x` in `s` such that `f x` equals `g x`. This is a variant of the Intermediate Value Theorem considering two functions `f` and `g`, stating in essence that the graphs of `f` and `g` must cross each other.
More concisely: Given a preconnected set in a topological space with a linear ordering and an order-closed type, if two continuous functions `f` and `g` satisfy `f a <= g a` for some `a` in the set and `g b <= f b` for some `b` in the set, then there exists a point `x` in the set such that `f x = g x`.
|
IsPreconnected.Icc_subset
theorem IsPreconnected.Icc_subset :
∀ {α : Type v} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderClosedTopology α] {s : Set α},
IsPreconnected s → ∀ {a b : α}, a ∈ s → b ∈ s → Set.Icc a b ⊆ s
The theorem `IsPreconnected.Icc_subset` states that, for any preconnected set `s` in a linearly ordered topological space with an order-closed topology, if `s` contains the endpoints `a` and `b` of a closed interval (i.e., `a` and `b` both belong to `s`), then `s` also contains the entire closed interval from `a` to `b`. In other words, all values `x` for which `a ≤ x ≤ b` also belong to `s`. This means that preconnected sets in such a space have the property that whenever they contain the endpoints of a closed interval, they also contain all points in between those endpoints.
More concisely: In a linearly ordered topological space with order-closed topology, if a preconnected set contains the endpoints of a closed interval, then it contains the entire closed interval.
|
intermediate_value_Icc
theorem intermediate_value_Icc :
∀ {α : Type u} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ]
[inst_6 : OrderClosedTopology δ] {a b : α},
a ≤ b → ∀ {f : α → δ}, ContinuousOn f (Set.Icc a b) → Set.Icc (f a) (f b) ⊆ f '' Set.Icc a b
The **Intermediate Value Theorem** for functions in Lean 4 states that for any conditionally complete linearly ordered topological space 'α' and any linearly ordered topological space 'δ', if 'a' and 'b' are elements of 'α' such that 'a' is less than or equal to 'b', and if 'f' is a function from 'α' to 'δ' that is continuous on the closed interval from 'a' to 'b', then the closed interval from 'f(a)' to 'f(b)' in 'δ' is a subset of the image of 'f' on the closed interval from 'a' to 'b' in 'α'. In other words, if a function is continuous on a closed interval, then for any value between the function's values at the endpoints of the interval, there is a point in the interval where the function takes this value.
More concisely: If a continuous function on a closed interval in a linearly ordered topological space maps the endpoints to values in another linearly ordered topological space, then it takes on every value between these endpoints within the interval.
|
intermediate_value_univ
theorem intermediate_value_univ :
∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
[inst_3 : OrderClosedTopology α] [inst_4 : PreconnectedSpace X] (a b : X) {f : X → α},
Continuous f → Set.Icc (f a) (f b) ⊆ Set.range f
This theorem is the **Intermediate Value Theorem** for continuous functions on connected spaces. It states that for any topological space `X`, with a preconnected topology, and a linearly ordered topological space `α`, with an order closed topology, given two points `a` and `b` in `X`, and a continuous function `f` from `X` to `α`, the closed interval `[f(a), f(b)]` is a subset of the range of the function `f`. In other words, for any value between `f(a)` and `f(b)`, there exists a point in `X` such that the function `f` at that point equals that value. This theorem captures the intuition that a continuous function does not "skip" any values in between its endpoints on a connected space.
More concisely: For a continuous function `f` from a connected topological space `X` to a linearly ordered topological space `α` with an order closed topology, if `a` and `b` are points in `X` such that `f(a)` and `f(b)` are comparable in `α`, then the interval `[f(a), f(b)]` is contained in the range of `f`.
|
intermediate_value_Icc'
theorem intermediate_value_Icc' :
∀ {α : Type u} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ]
[inst_6 : OrderClosedTopology δ] {a b : α},
a ≤ b → ∀ {f : α → δ}, ContinuousOn f (Set.Icc a b) → Set.Icc (f b) (f a) ⊆ f '' Set.Icc a b
This is the **Intermediate Value Theorem** for continuous functions on closed intervals. Given a conditionally complete linearly ordered topological space `α`, a linearly ordered topological space `δ` that is densely ordered, a function `f` from `α` to `δ` that is continuous on the closed interval from `a` to `b` in `α`, and provided that `a` is less than or equal to `b`, then the closed interval from `f(b)` to `f(a)` in `δ` is a subset of the image of the function `f` on the closed interval from `a` to `b`. This theorem applies specifically to the case where `f(a)` is greater than or equal to a given value `t` which is greater than or equal to `f(b)`. This essentially means that if `f` is continuous on a closed interval, then `f` takes on every value between `f(a)` and `f(b)`, inclusive.
More concisely: If a continuous function `f` maps a closed interval in a linearly ordered topological space to another linearly ordered topological space, and `a` and `b` are the endpoints of the interval with `a ≤ b`, then the closed interval between `f(a)` and `f(b)` contains every value that `f` takes on some point `x` in the interval `[a, b]`.
|
mem_range_of_exists_le_of_exists_ge
theorem mem_range_of_exists_le_of_exists_ge :
∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
[inst_3 : OrderClosedTopology α] [inst_4 : PreconnectedSpace X] {c : α} {f : X → α},
Continuous f → (∃ a, f a ≤ c) → (∃ b, c ≤ f b) → c ∈ Set.range f
This theorem is a formal statement of the Intermediate Value Theorem for continuous functions on connected spaces. Given a topological space `X`, a linear ordered topological space `α` with an order-closed topology, and assuming `X` is preconnected, the theorem states that for any real number `c` and any continuous function `f` from `X` to `α`, if there exists an `a` in `X` such that `f(a) ≤ c`, and there exists a `b` in `X` such that `c ≤ f(b)`, then `c` must be in the range of `f`. In other words, if `c` is a value between `f(a)` and `f(b)`, then there must be some `x` in the domain of `f` for which `f(x) = c`.
More concisely: If a continuous function between a connected and preconnected topological space and a linearly ordered topological space with order-closed topology maps two order-comparable elements to different order-comparable values, then it must map some element to the value in between.
|
IsPreconnected.eq_univ_of_unbounded
theorem IsPreconnected.eq_univ_of_unbounded :
∀ {α : Type v} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderClosedTopology α] {s : Set α},
IsPreconnected s → ¬BddBelow s → ¬BddAbove s → s = Set.univ
This theorem states that in a linearly ordered topological space that also has the property of being an order-closed topology, if a preconnected set is unbounded both below and above, then it must be the entire space. In other words, for such a topological structure, there can be no preconnected set that is unbounded in both directions without it encompassing every point in the space.
More concisely: In a linearly ordered topological space with an order-closed topology, a preconnected and unbounded set is the entire space.
|
isPreconnected_Ioo
theorem isPreconnected_Ioo :
∀ {α : Type u} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] {a b : α}, IsPreconnected (Set.Ioo a b)
The theorem `isPreconnected_Ioo` states that for any type `α` that is a conditionally complete linear order, has a topological space structure, an order topology, and is densely ordered, the left-open right-open interval `(a, b)` (i.e., the set of elements `x` such that `a < x < b`) is preconnected. In terms of topology, a preconnected set is one where there is no non-trivial open partition, meaning it cannot be expressed as the union of two disjoint non-empty open sets. Thus, the theorem says that any open interval in such a space cannot be split into two disjoint non-empty open sets.
More concisely: In a densely ordered, conditionally complete linear order `α` with a topology making it a topological space, the left-open right-open interval `(a, b)` is preconnected, meaning it cannot be expressed as the union of two disjoint non-empty open sets.
|
Continuous.surjective
theorem Continuous.surjective :
∀ {α : Type u} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ]
[inst_6 : OrderClosedTopology δ] {f : α → δ},
Continuous f →
Filter.Tendsto f Filter.atTop Filter.atTop →
Filter.Tendsto f Filter.atBot Filter.atBot → Function.Surjective f
This theorem asserts that if you have a continuous function `f` from a type `α` to another type `δ` and both `α` and `δ` are equipped with a conditionally complete linear order, a topological space structure, and an order topology, and `α` is densely ordered, and `δ` has an order-closed topology, then if the function `f` has the property that it tends to infinity (`Filter.atTop`) along the infinite sequence in `α` (`Filter.atTop`), and tends to negative infinity (`Filter.atBot`) along the sequence tending to negative infinity in `α` (`Filter.atBot`), then `f` is a surjective function. In other words, for every element in `δ`, there exists an element in `α` such that `f` maps this element in `α` to that specific element in `δ`.
More concisely: If `f` is a continuous function from a densely ordered, conditionally complete linear order `α` with an order topology and an order-closed topology to another such order `δ`, and `f` tends to infinity on sequences tending to infinity in `α` and to negative infinity on sequences tending to negative infinity in `α`, then `f` is surjective.
|
IsPreconnected.intermediate_value₂_eventually₂
theorem IsPreconnected.intermediate_value₂_eventually₂ :
∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
[inst_3 : OrderClosedTopology α] {s : Set X},
IsPreconnected s →
∀ {l₁ l₂ : Filter X} [inst_4 : l₁.NeBot] [inst_5 : l₂.NeBot],
l₁ ≤ Filter.principal s →
l₂ ≤ Filter.principal s →
∀ {f g : X → α},
ContinuousOn f s → ContinuousOn g s → l₁.EventuallyLE f g → l₂.EventuallyLE g f → ∃ x ∈ s, f x = g x
This theorem states that for any topological space `X`, any linearly ordered type `α` that is also a topological space and has an order-closed topology, and any preconnected set `s` of `X`, the following is true: for any two non-bottom filters `l₁` and `l₂` which are subsets of the principal filter of `s`, and for any two functions `f` and `g` from `X` to `α` that are continuous on `s`, if `f` is less than or equal to `g` almost everywhere with respect to `l₁` and `g` is less than or equal to `f` almost everywhere with respect to `l₂`, then there exists an element `x` in `s` such that `f(x) = g(x)`.
In simpler terms, if `f` and `g` are two functions that are continuous on a preconnected set and each is not greater than the other almost everywhere with respect to some filters, then they must intersect at some point in the set. This theorem is a version of the intermediate value theorem for sets in a topological space.
More concisely: Given a topological space X, a preconnected set s, and two continuous functions f and g from X to a linearly ordered topological space α with order-closed topology, if f is less than or equal to g almost everywhere with respect to some filters l₁ and g is less than or equal to f almost everywhere with respect to some filters l₂, then there exists an x in s such that f(x) = g(x).
|
ContinuousOn.surjOn_Icc
theorem ContinuousOn.surjOn_Icc :
∀ {α : Type u} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ]
[inst_6 : OrderClosedTopology δ] {s : Set α} [hs : s.OrdConnected] {f : α → δ},
ContinuousOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → Set.SurjOn f s (Set.Icc (f a) (f b))
The Intermediate Value Theorem states that if a function 'f' is continuous on an order-connected set 's', and 'a' and 'b' are two points within this set, then the function 'f' maps the set 's' to a superset of the closed interval between 'f(a)' and 'f(b)'. In other words, the image of 's' under 'f' contains all values of 'f' between 'f(a)' and 'f(b)', inclusive. This theorem applies to any function whose domain is a conditionally complete linear order (a system that allows any nonempty set that is bounded above to have a least upper bound), and whose codomain is a linear order (a system that allows any two elements to be compared) where both spaces are equipped with a topological structure.
More concisely: If a continuous function 'f' maps an order-connected, conditionally complete linear order set 's' to a linear order set, then the image of 's' under 'f' contains all values between 'f(a)' and 'f(b)', inclusive, for any 'a, b' in 's'.
|
IsPreconnected.intermediate_value₂_eventually₁
theorem IsPreconnected.intermediate_value₂_eventually₁ :
∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
[inst_3 : OrderClosedTopology α] {s : Set X},
IsPreconnected s →
∀ {a : X} {l : Filter X},
a ∈ s →
∀ [inst_4 : l.NeBot],
l ≤ Filter.principal s →
∀ {f g : X → α},
ContinuousOn f s → ContinuousOn g s → f a ≤ g a → l.EventuallyLE g f → ∃ x ∈ s, f x = g x
This theorem states that for any preconnected subset 's' of a topological space 'X' and any two continuous functions 'f' and 'g' from 'X' to a linearly ordered, topologically closed space 'α', if 'f' is less than or equal to 'g' at a point 'a' in 's' and 'g' is eventually less than or equal to 'f' in a filter 'l' which is a superset of 's', then there exists a point in 's' at which 'f' equals 'g'. Note that the filter 'l' must be non-empty ('Filter.NeBot l').
More concisely: If a preconnected subset 's' of a topological space 'X' and continuous functions 'f' and 'g' from 'X' to a linearly ordered, topologically closed space 'α' satisfy 'f'(a) <= 'g'(a) in 's' and 'g' is eventually less than or equal to 'f' in a non-empty filter 'l' that supersets 's', then there exists a point in 's' where 'f' equals 'g'.
|
IsClosed.mem_of_ge_of_forall_exists_gt
theorem IsClosed.mem_of_ge_of_forall_exists_gt :
∀ {α : Type u} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
{a b : α} {s : Set α},
IsClosed (s ∩ Set.Icc a b) → a ∈ s → a ≤ b → (∀ x ∈ s ∩ Set.Ico a b, (s ∩ Set.Ioc x b).Nonempty) → b ∈ s
This theorem is a form of "continuous induction principle" for a closed interval. It states that, for a given set `s` and two values `a` and `b` in a conditionally complete linear order space with a topological structure, if the intersection of `s` and the closed interval between `a` and `b` forms a closed set, and `a` is an element of `s` and `a` is less than or equal to `b`, and for every `x` in the intersection of `s` and the half-open interval from `a` up to but not including `b`, there exists an element in the intersection of `s` and the half-open interval from `x` (exclusive) to `b` (inclusive), then `b` is also an element of `s`. In other words, if the set `s` intersects the closed interval `[a, b]`, contains `a`, and the set `s` intersected with the half-open interval `[a, b)` has no maximal point, then `b` belongs to `s`.
More concisely: If a set `s` intersects the closed interval `[a, b]` in a conditionally complete linear order space with a topology, `a` is in `s`, and every half-open interval `[a, x)` in `s` has a lower bound in `s`, then `b` is also in `s`.
|