English
If f is monotone on s and on t, with s to the left of t and c is the center, then f is monotone on s ∪ t.
Русский
Если f монотонна на s и t, причём s слева от t и есть центр c, тогда f монотонна на s ∪ t.
LaTeX
$$$(h_1: MonotoneOn\ f\ s) \land (h_2: MonotoneOn\ f\ t) \land (hs: IsGreatest s c) \land (ht: IsLeast t c) \rightarrow MonotoneOn f (s \cup t)$$$
Lean4
/-- If `f` is strictly antitone both on `s` and `t`, with `s` to the left of `t` and the center
point belonging to both `s` and `t`, then `f` is strictly antitone on `s ∪ t` -/
protected theorem union {s t : Set α} {c : α} (h₁ : StrictAntiOn f s) (h₂ : StrictAntiOn f t) (hs : IsGreatest s c)
(ht : IsLeast t c) : StrictAntiOn f (s ∪ t) :=
(h₁.dual_right.union h₂.dual_right hs ht).dual_right
