Ioo — Mathlib

English

If f is monotone on a set s and g is antitone on s, then the interval-valued function x ↦ Ioo(f(x), g(x)) is antitone on s; i.e., for x ≤ y in s, Ioo(f(x), g(x)) ⊆ Ioo(f(y), g(y)).

Русский

Если f монотонна на множестве s, а g антитонна на s, то отображение x ↦ Ioo(f(x), g(x)) антитонируется на s: при x ≤ y имеем Ioo(f(x), g(x)) ⊆ Ioo(f(y), g(y)).

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 : MonotoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun x => Ioo (f x) (g x)) s :=
  hf.Ioi.inter hg.Iio

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