English
Let f, g be functions from α to β and s a subset of α. If f is antitone on s and g is monotone on s, then the set-valued map x ↦ Ioc(f(x), g(x)) is monotone on s; i.e., for all x ≤ y with x, y ∈ s, Ioc(f(x), g(x)) ⊆ Ioc(f(y), g(y)).
Русский
Пусть f, g : α → β и s ⊆ α. Если f убывает на s, а g возрастает на s, то отображение x ↦ Ioc(f(x), g(x)) с точки зрения включения множеств неубывает на s; то есть при x ≤ y и x, y ∈ s выполняется Ioc(f(x), g(x)) ⊆ Ioc(f(y), g(y)).
LaTeX
$$$\forall x \in s\,\forall y \in s\, (x \le y) \Rightarrow \mathrm{Ioc}(f(x), g(x)) \subseteq \mathrm{Ioc}(f(y), g(y)).$$$
Lean4
protected theorem Ioc (hf : AntitoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => Ioc (f x) (g x)) s :=
hf.Ioi.inter hg.Iic
