Documentation

Mathlib.Topology.Algebra.Order.ExtrClosure

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} [] [] [] {f : XY} {s : Set X} {a : X} (h : IsMaxOn f s a) (hc : ContinuousOn f ()) :
IsMaxOn f () a
theorem IsMinOn.closure {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} {s : Set X} {a : X} (h : IsMinOn f s a) (hc : ContinuousOn f ()) :
IsMinOn f () a
theorem IsExtrOn.closure {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} {s : Set X} {a : X} (h : IsExtrOn f s a) (hc : ContinuousOn f ()) :
IsExtrOn f () a
theorem IsLocalMaxOn.closure {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} {s : Set X} {a : X} (h : IsLocalMaxOn f s a) (hc : ContinuousOn f ()) :
theorem IsLocalMinOn.closure {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} {s : Set X} {a : X} (h : IsLocalMinOn f s a) (hc : ContinuousOn f ()) :
theorem IsLocalExtrOn.closure {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} {s : Set X} {a : X} (h : ) (hc : ContinuousOn f ()) :