image_Ici_subset

Mathlib.Order.Interval.Set.Image

URI: https://scilib.ai/kg/mathlib#Antitone.image_Ici_subset

English

If f is Antitone, then the image of all x with x ≥ a lies in (-∞, f(a)].

Русский

Если f антитонична, то образ x ≥ a лежит в (-∞, f(a)].

LaTeX

$$$f(Ici a) \subseteq Iic(f(a))$$$

Lean4

theorem image_Ici_subset (h : Antitone f) : f '' Ici a ⊆ Iic (f a) :=
  (h.antitoneOn _).image_Ici_subset

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

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

Разделы

Аффилиация

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