English
If h is antitone on s and its values on s are bounded below and above, then there exists an antitone extension to the whole space agreeing with h on s.
Русский
Если h антито́нна на s и значения на s ограничены снизу и сверху, то существует антитоническое продолжение повсюду, совпадающее на s.
LaTeX
$$$\text{AntitoneOn } f s \land BddBelow (f''s) \land BddAbove (f''s) \Rightarrow \exists g:\alpha \to \beta,\ (\mathrm{Antitone}\ g) \land \mathrm{EqOn}\ f\ g\ s$$$
Lean4
/-- If a function is antitone and is bounded on a set `s`, then it admits an antitone extension to
the whole space. -/
theorem exists_antitone_extension (h : AntitoneOn f s) (hl : BddBelow (f '' s)) (hu : BddAbove (f '' s)) :
∃ g : α → β, Antitone g ∧ EqOn f g s :=
h.dual_right.exists_monotone_extension hu hl
