English
If f is monotone on s and t, then monotone on s ∪ t provided the order context.
Русский
Если f монотонна на s и t, то монотонна на s ∪ t при соблюдении условий порядка.
LaTeX
$$$MonotoneOn\ f\ s \land MonotoneOn\ f\ t \land IsGreatest\ s\ c \land IsLeast\ t\ c \Rightarrow MonotoneOn\ f\ (s \cup t)$$$
Lean4
/-- If `f` is monotone 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 monotone on `s ∪ t` -/
protected theorem union_right {s t : Set α} {c : α} (h₁ : MonotoneOn f s) (h₂ : MonotoneOn f t) (hs : IsGreatest s c)
(ht : IsLeast t c) : MonotoneOn f (s ∪ t) :=
by
have A : ∀ x, x ∈ s ∪ t → x ≤ c → x ∈ s := by
intro x hx hxc
cases hx
· assumption
rcases eq_or_lt_of_le hxc with (rfl | h'x)
· exact hs.1
exact (lt_irrefl _ (h'x.trans_le (ht.2 (by assumption)))).elim
have B : ∀ x, x ∈ s ∪ t → c ≤ x → x ∈ t := by
intro x hx hxc
match hx with
| Or.inr hx => exact hx
| Or.inl hx =>
rcases eq_or_lt_of_le hxc with (rfl | h'x)
· exact ht.1
exact (lt_irrefl _ (h'x.trans_le (hs.2 hx))).elim
intro x hx y hy hxy
rcases lt_or_ge x c with (hxc | hcx)
· have xs : x ∈ s := A _ hx hxc.le
rcases lt_or_ge y c with (hyc | hcy)
· exact h₁ xs (A _ hy hyc.le) hxy
· exact (h₁ xs hs.1 hxc.le).trans (h₂ ht.1 (B _ hy hcy) hcy)
· have xt : x ∈ t := B _ hx hcx
have yt : y ∈ t := B _ hy (hcx.trans hxy)
exact h₂ xt yt hxy
