Ioc — Mathlib

English

Let f be monotone on s and g antitone on s. Then x ∈ s → Ioc(f x, g x) is antitone on s.

Русский

Пусть f монотонна на s, а g антимонотонна на s. Тогда x ∈ s → Ioc(f x, g x) антитонично по x.

LaTeX

$$$\forall x,y \in s,\ x \le y \Rightarrow \Ioc(f(y))(g(y)) \subseteq \Ioc(f(x))(g(x)).$$$

Lean4

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

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