Maximum/minimum on the closure of a set #
In this file we prove several versions of the following statement: if f : X → Y has a (local or
not) maximum (or minimum) on a set s at a point a and is continuous on the closure of s, then
f has an extremum of the same type on Closure s at a.
theorem
IsMaxOn.closure
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[Preorder Y]
[OrderClosedTopology Y]
{f : X → Y}
{s : Set X}
{a : X}
(h : IsMaxOn f s a)
(hc : ContinuousOn f (closure s))
:
theorem
IsMinOn.closure
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[Preorder Y]
[OrderClosedTopology Y]
{f : X → Y}
{s : Set X}
{a : X}
(h : IsMinOn f s a)
(hc : ContinuousOn f (closure s))
:
theorem
IsExtrOn.closure
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[Preorder Y]
[OrderClosedTopology Y]
{f : X → Y}
{s : Set X}
{a : X}
(h : IsExtrOn f s a)
(hc : ContinuousOn f (closure s))
:
theorem
IsLocalMaxOn.closure
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[Preorder Y]
[OrderClosedTopology Y]
{f : X → Y}
{s : Set X}
{a : X}
(h : IsLocalMaxOn f s a)
(hc : ContinuousOn f (closure s))
:
IsLocalMaxOn f (closure s) a
theorem
IsLocalMinOn.closure
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[Preorder Y]
[OrderClosedTopology Y]
{f : X → Y}
{s : Set X}
{a : X}
(h : IsLocalMinOn f s a)
(hc : ContinuousOn f (closure s))
:
IsLocalMinOn f (closure s) a
theorem
IsLocalExtrOn.closure
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[Preorder Y]
[OrderClosedTopology Y]
{f : X → Y}
{s : Set X}
{a : X}
(h : IsLocalExtrOn f s a)
(hc : ContinuousOn f (closure s))
:
IsLocalExtrOn f (closure s) a