English
If f is antitone on s and t, with s to the left of t and center in both, then f is antitone on s ∪ t.
Русский
Если f антитонна на s и t, причём s слева от t и центр принадлежит обеим, тогда f антитонна на s ∪ t.
LaTeX
$$$\mathrm{AntitoneOn}(f,s) \land \mathrm{AntitoneOn}(f,t) \land IsGreatest\ s\ c \land IsLeast\ t\ c \rightarrow \mathrm{AntitoneOn}(f, s \cup t)$$$
Lean4
/-- If `f` is 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 antitone on `s ∪ t` -/
protected theorem union_right {s t : Set α} {c : α} (h₁ : AntitoneOn f s) (h₂ : AntitoneOn f t) (hs : IsGreatest s c)
(ht : IsLeast t c) : AntitoneOn f (s ∪ t) :=
(h₁.dual_right.union_right h₂.dual_right hs ht).dual_right
