Extension of a monotone function from a set to the whole space #
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
MonotoneOn.exists_monotone_extension
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[ConditionallyCompleteLinearOrder β]
{f : α → β}
{s : Set α}
(h : MonotoneOn f s)
(hl : BddBelow (f '' s))
(hu : BddAbove (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
AntitoneOn.exists_antitone_extension
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[ConditionallyCompleteLinearOrder β]
{f : α → β}
{s : Set α}
(h : AntitoneOn f s)
(hl : BddBelow (f '' s))
(hu : BddAbove (f '' s))
:
If a function is antitone and is bounded on a set s, then it admits an antitone extension to
the whole space.