image_Ioc_subset — Mathlib

English

Let f be strictly order-reversing. Then for any a, b, the image of the half-open interval Ioc(a, b) under f is contained in the half-open interval Ico(f(b), f(a)).

Русский

Пусть f — строго антимонотонная функция. Тогда для любых a, b образ полузакрытого интервала Ioc(a, b) под f содержится в интервале Ico(f(b), f(a)).

LaTeX

$$$ f''\mathrm{Ioc}(a,b) \subseteq \mathrm{Ico}(f(b), f(a)) $$$

Lean4

theorem image_Ioc_subset (h : StrictAnti f) : f '' Ioc a b ⊆ Ico (f b) (f a) :=
  (h.strictAntiOn _).image_Ioc_subset

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