Maximum/minimum on the closure of a set #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
@[protected]
theorem
is_max_on.closure
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
[topological_space Y]
[preorder Y]
[order_closed_topology Y]
{f : X → Y}
{s : set X}
{a : X}
(h : is_max_on f s a)
(hc : continuous_on f (closure s)) :
@[protected]
theorem
is_min_on.closure
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
[topological_space Y]
[preorder Y]
[order_closed_topology Y]
{f : X → Y}
{s : set X}
{a : X}
(h : is_min_on f s a)
(hc : continuous_on f (closure s)) :
@[protected]
theorem
is_extr_on.closure
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
[topological_space Y]
[preorder Y]
[order_closed_topology Y]
{f : X → Y}
{s : set X}
{a : X}
(h : is_extr_on f s a)
(hc : continuous_on f (closure s)) :
is_extr_on f (closure s) a
@[protected]
theorem
is_local_max_on.closure
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
[topological_space Y]
[preorder Y]
[order_closed_topology Y]
{f : X → Y}
{s : set X}
{a : X}
(h : is_local_max_on f s a)
(hc : continuous_on f (closure s)) :
is_local_max_on f (closure s) a
@[protected]
theorem
is_local_min_on.closure
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
[topological_space Y]
[preorder Y]
[order_closed_topology Y]
{f : X → Y}
{s : set X}
{a : X}
(h : is_local_min_on f s a)
(hc : continuous_on f (closure s)) :
is_local_min_on f (closure s) a
@[protected]
theorem
is_local_extr_on.closure
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
[topological_space Y]
[preorder Y]
[order_closed_topology Y]
{f : X → Y}
{s : set X}
{a : X}
(h : is_local_extr_on f s a)
(hc : continuous_on f (closure s)) :
is_local_extr_on f (closure s) a