# mathlib3documentation

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} [preorder Y] {f : X Y} {s : set X} {a : X} (h : s a) (hc : (closure s)) :
(closure s) a
@[protected]
theorem is_min_on.closure {X : Type u_1} {Y : Type u_2} [preorder Y] {f : X Y} {s : set X} {a : X} (h : s a) (hc : (closure s)) :
(closure s) a
@[protected]
theorem is_extr_on.closure {X : Type u_1} {Y : Type u_2} [preorder Y] {f : X Y} {s : set X} {a : X} (h : s a) (hc : (closure s)) :
(closure s) a
@[protected]
theorem is_local_max_on.closure {X : Type u_1} {Y : Type u_2} [preorder Y] {f : X Y} {s : set X} {a : X} (h : a) (hc : (closure s)) :
(closure s) a
@[protected]
theorem is_local_min_on.closure {X : Type u_1} {Y : Type u_2} [preorder Y] {f : X Y} {s : set X} {a : X} (h : a) (hc : (closure s)) :
(closure s) a
@[protected]
theorem is_local_extr_on.closure {X : Type u_1} {Y : Type u_2} [preorder Y] {f : X Y} {s : set X} {a : X} (h : a) (hc : (closure s)) :
(closure s) a