Ioo — Mathlib

English

Let f be monotone and g be antitone from α to β. Then the map x ↦ Ioo(f(x), g(x)) is antitone; i.e., for all x ≤ y, Ioo(f(x), g(x)) ⊇ Ioo(f(y), g(y)).

Русский

Пусть f монотонно возрастает, а g антитонно. Тогда отображение x ↦ Ioo(f(x), g(x)) антитонировано: при x ≤ y выполняется Ioo(f(x), g(x)) ⊇ Ioo(f(y), g(y)).

LaTeX

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

Lean4

protected theorem Ioo (hf : Monotone f) (hg : Antitone g) : Antitone fun x => Ioo (f x) (g x) :=
  hf.Ioi.inter hg.Iio

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