English
If f is strictly monotone on s and on t, and there is a center c with s greatest and t least, then f is strictly monotone on s ∪ t.
Русский
Если f строго монотонна на s и на t, и существует центр c так, что s имеет наибольший элемент c и t имеет наименьший элемент c, тогда f строго монотонна на s ∪ t.
LaTeX
$$$(h_1 : StrictMonoOn f s) \rightarrow (h_2 : StrictMonoOn f t) \rightarrow (hs : IsGreatest s c) (ht : IsLeast t c) \rightarrow StrictMonoOn f (s \cup t)$$$
Lean4
/-- If `f` is strictly 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 strictly monotone on `s ∪ t` -/
protected theorem union {s t : Set α} {c : α} (h₁ : StrictMonoOn f s) (h₂ : StrictMonoOn f t) (hs : IsGreatest s c)
(ht : IsLeast t c) : StrictMonoOn 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).trans_le (h₂.monotoneOn ht.1 (B _ hy hcy) hcy)
· have xt : x ∈ t := B _ hx hcx
have yt : y ∈ t := B _ hy (hcx.trans hxy.le)
exact h₂ xt yt hxy
