image_uIcc_subset

Mathlib.Order.Interval.Set.UnorderedInterval

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

English

If f is antitone, then f image of uIcc(a,b) is contained in uIcc(f(a), f(b)).

Русский

Если f антитонна, то образ f(uIcc(a,b)) содержится в uIcc(f(a), f(b)).

LaTeX

$$$ (hf : Antitone f) \\Rightarrow f '' uIcc a b \\subseteq uIcc (f a) (f b) $$$

Lean4

theorem _root_.Antitone.image_uIcc_subset (hf : Antitone f) : f '' uIcc a b ⊆ uIcc (f a) (f b) :=
  (hf.antitoneOn _).image_uIcc_subset

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

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

Разделы

Аффилиация

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