exists_Ioo_extr_on_Icc
theorem exists_Ioo_extr_on_Icc :
∀ {X : Type u_1} {Y : Type u_2} [inst : ConditionallyCompleteLinearOrder X] [inst_1 : DenselyOrdered X]
[inst_2 : TopologicalSpace X] [inst_3 : OrderTopology X] [inst_4 : LinearOrder Y] [inst_5 : TopologicalSpace Y]
[inst_6 : OrderTopology Y] {f : X → Y} {a b : X},
a < b → ContinuousOn f (Set.Icc a b) → f a = f b → ∃ c ∈ Set.Ioo a b, IsExtrOn f (Set.Icc a b) c
The theorem `exists_Ioo_extr_on_Icc` states that for any types `X` and `Y`, where `X` has a conditionally complete linear order and a densely ordered topological space with order topology, and `Y` is a linearly ordered topological space with order topology, if `f` is a continuous function on the closed interval from `a` to `b` (`a` less than `b`) in `X` such that `f(a)` equals `f(b)`, then there exists a point `c` in the open interval from `a` to `b` (`a` less than `b`) such that `f` reaches either its maximum or minimum value at `c` on the closed interval from `a` to `b`.
More concisely: Given a type `X` with a conditionally complete linear order and a densely ordered topology, and a linearly ordered topological space `Y`, if `f: X ↔ Y` is a continuous function with `a < b` in `X` such that `f(a) = f(b)`, then there exists `c` in the open interval `(a, b)` such that `f` attains its maximum or minimum on `[a, b]`.
|
exists_isExtrOn_Ioo_of_tendsto
theorem exists_isExtrOn_Ioo_of_tendsto :
∀ {X : Type u_1} {Y : Type u_2} [inst : ConditionallyCompleteLinearOrder X] [inst_1 : DenselyOrdered X]
[inst_2 : TopologicalSpace X] [inst_3 : OrderTopology X] [inst_4 : LinearOrder Y] [inst_5 : TopologicalSpace Y]
[inst_6 : OrderTopology Y] {f : X → Y} {a b : X} {l : Y},
a < b →
ContinuousOn f (Set.Ioo a b) →
Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds l) →
Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds l) → ∃ c ∈ Set.Ioo a b, IsExtrOn f (Set.Ioo a b) c
The theorem `exists_isExtrOn_Ioo_of_tendsto` states that for any function `f` mapping from a conditionally complete linear ordered topological space `X` to a linear ordered topological space `Y`, if `f` is continuous on an open interval `(a, b)` where `a` and `b` are distinct points in `X`, and if the limit of `f` as it approaches `a` from values greater than `a` and as it approaches `b` from values less than `b` both equal to the same value `l` in `Y`, then there exists a point `c` in the open interval `(a, b)` on which `f` attains an extremum (minimum or maximum) on this interval. This theorem encapsulates the idea that a continuous function on an open interval, which tends to the same value at its endpoints, must have a point in the interval where it reaches a maximum or minimum value.
More concisely: If a continuous function on an open interval of a conditionally complete linear ordered topological space attains the same limit at its distinct endpoints, then there exists an extremum point in the interval.
|
exists_isLocalExtr_Ioo
theorem exists_isLocalExtr_Ioo :
∀ {X : Type u_1} {Y : Type u_2} [inst : ConditionallyCompleteLinearOrder X] [inst_1 : DenselyOrdered X]
[inst_2 : TopologicalSpace X] [inst_3 : OrderTopology X] [inst_4 : LinearOrder Y] [inst_5 : TopologicalSpace Y]
[inst_6 : OrderTopology Y] {f : X → Y} {a b : X},
a < b → ContinuousOn f (Set.Icc a b) → f a = f b → ∃ c ∈ Set.Ioo a b, IsLocalExtr f c
The theorem `exists_isLocalExtr_Ioo` states that given a conditionally complete linear order `X`, which is densely ordered and has a topological structure that is compatible with its order structure, and a linear order `Y` with a topological structure that is compatible with its order, for any continuous function `f` from `X` to `Y` and any two distinct points `a` and `b` from `X`, if `f` is continuous on the closed interval between `a` and `b` (including `a` and `b`) and `f(a)` equals `f(b)`, then there exists a point `c` in the open interval between `a` and `b` (excluding `a` and `b`) such that `c` is a local extremum of `f`, which means `f(c)` is either a local minimum or a local maximum.
More concisely: Given a continuous function between two densely ordered topological spaces with compatible order and topological structures, if the function is equal on two distinct points in a closed interval and is continuous on that interval, then there exists a point in the open interval between them that is a local extremum.
|
exists_isLocalExtr_Ioo_of_tendsto
theorem exists_isLocalExtr_Ioo_of_tendsto :
∀ {X : Type u_1} {Y : Type u_2} [inst : ConditionallyCompleteLinearOrder X] [inst_1 : DenselyOrdered X]
[inst_2 : TopologicalSpace X] [inst_3 : OrderTopology X] [inst_4 : LinearOrder Y] [inst_5 : TopologicalSpace Y]
[inst_6 : OrderTopology Y] {f : X → Y} {a b : X} {l : Y},
a < b →
ContinuousOn f (Set.Ioo a b) →
Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds l) →
Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds l) → ∃ c ∈ Set.Ioo a b, IsLocalExtr f c
The theorem `exists_isLocalExtr_Ioo_of_tendsto` states that given a function `f` from a topological space `X` to another topological space `Y`, both equipped with a linear ordering and an order-induced topology, and two points `a` and `b` in `X` such that `a < b`, if `f` is continuous on the open interval between `a` and `b`, and `f` tends to the same limit `l` at both `a` and `b` (considering values of `f` only to the right of `a` and to the left of `b`), then there exists a point `c` in the open interval between `a` and `b` where `f` attains a local extremum (either a local minimum or a local maximum).
More concisely: Given a continuous function `f` between ordered topological spaces `X` and `Y` with `a < b` in `X`, if `f` tends to the same limit at `a` and `b`, then there exists a local extremum of `f` in the open interval `(a, b)`.
|