Iic_union_Ici — Mathlib

English

If f is strictly monotone on Iic a and on Ici a, then f is strictly monotone on the whole line.

Русский

Если f строго монотонна на Iic a и на Ici a, то она строго монотонна на всей прямой.

LaTeX

$$$StrictMonoOn\ f\ (Iic\ a) \rightarrow StrictMonoOn\ f\ (Ici\ a) \rightarrow StrictMono\ f$$$

Lean4

/-- If `f` is strictly monotone both on `(-∞, a]` and `[a, ∞)`, then it is strictly monotone on the
whole line. -/
protected theorem Iic_union_Ici (h₁ : StrictMonoOn f (Iic a)) (h₂ : StrictMonoOn f (Ici a)) : StrictMono f :=
  by
  rw [← strictMonoOn_univ, ← @Iic_union_Ici _ _ a]
  exact StrictMonoOn.union h₁ h₂ isGreatest_Iic isLeast_Ici

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