Ioo — Mathlib

English

If f is antitone and g is monotone, then the map x ↦ Ioo(f(x), g(x)) is monotone; i.e., for x ≤ y, Ioo(f(x), g(x)) ⊆ Ioo(f(y), g(y)).

Русский

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

LaTeX

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

Lean4

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

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