mathlib3 documentation

order.monotone.extension

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)) :
(g : α β), monotone g set.eq_on 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 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)) :
(g : α β), antitone g set.eq_on 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.