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} [PartialOrder α] [ConditionallyCompleteLinearOrder β] {f : α → β} {s : Set α} (h : MonotoneOn f s) (hl : BddBelow (f '' s)) (hu : BddAbove (f '' s)) : ∃ (g : α → β), Monotone g ∧ Set.EqOn f g 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} [PartialOrder α] [ConditionallyCompleteLinearOrder β] {f : α → β} {s : Set α} (h : AntitoneOn f s) (hl : BddBelow (f '' s)) (hu : BddAbove (f '' s)) : ∃ (g : α → β), Antitone g ∧ Set.EqOn f g s

If a function is antitone and is bounded on a set s, then it admits an antitone extension to the whole space.