English
If f is monotone on a set s and f(s) is bounded below and above, then there exists a monotone extension g to the whole domain with g|s = f.
Русский
Если f монотонна на множестве s и образ f(s) ограничен снизу и сверху, то существует монотонное продолжение g на всей области с g|s = f.
LaTeX
$$$\text{MonotoneOn } f s \land BddBelow (f''s) \land BddAbove (f''s) \Rightarrow \exists g:\alpha \to \beta,\ (\mathrm{Monotone}\ g) \land \mathrm{EqOn}\ f\ g\ s$$$
Lean4
/-- If a function is monotone and is bounded on a set `s`, then it admits a monotone extension to
the whole space. -/
theorem exists_monotone_extension (h : MonotoneOn f s) (hl : BddBelow (f '' s)) (hu : BddAbove (f '' s)) :
∃ g : α → β, Monotone g ∧ EqOn f g s := by
classical
/- The extension is defined by `f x = f a` for `x ≤ a`, and `f x` is the supremum of the values
of `f` to the left of `x` for `x ≥ a`. -/
rcases hl with ⟨a, ha⟩
have hu' : ∀ x, BddAbove (f '' (Iic x ∩ s)) := fun x => hu.mono (image_mono inter_subset_right)
let g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
have hgs : EqOn f g s := by
intro x hx
simp only [g]
have : IsGreatest (Iic x ∩ s) x := ⟨⟨right_mem_Iic, hx⟩, fun y hy => hy.1⟩
rw [if_neg this.nonempty.not_disjoint, ((h.mono inter_subset_right).map_isGreatest this).csSup_eq]
refine ⟨g, fun x y hxy => ?_, hgs⟩
by_cases hx : Disjoint (Iic x) s <;> by_cases hy : Disjoint (Iic y) s <;>
simp only [g, if_pos, if_neg, not_false_iff, *, refl]
· rcases not_disjoint_iff_nonempty_inter.1 hy with ⟨z, hz⟩
exact le_csSup_of_le (hu' _) (mem_image_of_mem _ hz) (ha <| mem_image_of_mem _ hz.2)
· exact (hx <| hy.mono_left <| Iic_subset_Iic.2 hxy).elim
· rw [not_disjoint_iff_nonempty_inter] at hx
gcongr; exacts [hu' _, hx.image _]
