Iic_union_Ici — Mathlib

English

If f is monotone on Iic a and on 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 strictly antitone both on `(-∞, a]` and `[a, ∞)`, then it is strictly antitone on the
whole line. -/
protected theorem Iic_union_Ici (h₁ : StrictAntiOn f (Iic a)) (h₂ : StrictAntiOn f (Ici a)) : StrictAnti f :=
  (h₁.dual_right.Iic_union_Ici h₂.dual_right).dual_right

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