Extension of a monotone function from a set to the whole space #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we prove that if a function is monotone and is bounded on a set s, then it admits a
monotone extension to the whole space.
theorem
monotone_on.exists_monotone_extension
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
{f : α → β}
{s : set α}
(h : monotone_on f s)
(hl : bdd_below (f '' s))
(hu : bdd_above (f '' s)) :
If a function is monotone and is bounded on a set s, then it admits a monotone extension to
the whole space.
theorem
antitone_on.exists_antitone_extension
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[conditionally_complete_linear_order β]
{f : α → β}
{s : set α}
(h : antitone_on f s)
(hl : bdd_below (f '' s))
(hu : bdd_above (f '' s)) :
If a function is antitone and is bounded on a set s, then it admits an antitone extension to
the whole space.