mathlib3 documentation

topology.algebra.order.extr_closure

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)) :
@[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)) :
@[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)) :
@[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)) :