English
If f is monotone on Iic a and on Ici a, then f is monotone on the whole line.
Русский
Если f монотонна на Iic a и на Ici a, то она монотонна на всей прямой.
LaTeX
$$$MonotoneOn\ f\ (Iic\ a) \rightarrow MonotoneOn\ f\ (Ici\ a) \rightarrow Monotone\ f$$$
Lean4
/-- If `f` is strictly antitone both on `(-∞, a]` and `[a, ∞)`, then it is strictly antitone on the
whole line. -/
protected theorem Iic_union_Ici (h₁ : StrictAntiOn f (Iic a)) (h₂ : StrictAntiOn f (Ici a)) : StrictAnti f :=
(h₁.dual_right.Iic_union_Ici h₂.dual_right).dual_right