Icc — Mathlib

English

Let f be monotone on s and g antitone on s. Then x ↦ Icc(f x, g x) is antitone on s.

Русский

Пусть f монотонна на s, а g антимонотонна на s. Тогда x ↦ Icc(f(x), g(x)) антитонична на s.

LaTeX

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

Lean4

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

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