Iic_union_Ici — Mathlib

English

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

Русский

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

LaTeX

$$$AntitoneOn\ f\ (Iic\ a) \Rightarrow AntitoneOn\ f\ (Ici\ a) \Rightarrow Antitone\ f$$$

Lean4

/-- If `f` is antitone both on `(-∞, a]` and `[a, ∞)`, then it is antitone on the whole line. -/
protected theorem Iic_union_Ici (h₁ : AntitoneOn f (Iic a)) (h₂ : AntitoneOn f (Ici a)) : Antitone f :=
  (h₁.dual_right.Iic_union_Ici h₂.dual_right).dual_right

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