Ioo — Mathlib

English

If f is antitone on s and g is monotone on s, then the set-valued map x ↦ Ioo(f(x), g(x)) is monotone on s.

Русский

Если f убывает на s, а g возрастает на s, то отображение x ↦ Ioo(f(x), g(x)) монотонно на s (по включению).

LaTeX

$$$\forall x,y \in s\ (x \le y) \Rightarrow \mathrm{Ioo}(f(x), g(x)) \subseteq \mathrm{Ioo}(f(y), g(y)).$$$

Lean4

protected theorem Ioo (hf : AntitoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => Ioo (f x) (g x)) s :=
  hf.Ioi.inter hg.Iio

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