Iic_union_Ici — Mathlib

English

If f is monotone on Iic a and 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 monotone both on `(-∞, a]` and `[a, ∞)`, then it is monotone on the whole line. -/
protected theorem Iic_union_Ici (h₁ : MonotoneOn f (Iic a)) (h₂ : MonotoneOn f (Ici a)) : Monotone f :=
  by
  rw [← monotoneOn_univ, ← @Iic_union_Ici _ _ a]
  exact MonotoneOn.union_right h₁ h₂ isGreatest_Iic isLeast_Ici

Похожие утверждения