image_Ioi_subset

Mathlib.Order.Interval.Set.Image

URI: https://scilib.ai/kg/mathlib#StrictAnti.image_Ioi_subset

English

If f is strictly antitone, then f maps the open interval (a, ∞) into (-∞, f(a)).

Русский

Если f строго антимонотонна, то образ (a, ∞) под f лежит в (-∞, f(a)).

LaTeX

$$$f(Ioi(a)) \subseteq Iio(f(a))$$$

Lean4

theorem image_Ioi_subset (h : StrictAnti f) : f '' Ioi a ⊆ Iio (f a) :=
  (h.strictAntiOn _).image_Ioi_subset

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru