image_strictAnti

Mathlib.Logic.Equiv.Set

URI: https://scilib.ai/kg/mathlib#Equiv.image_strictAnti

English

If e is strictly antitone, then the restricted map on s is strictly antitone: x < y implies e(x) > e(y).

Русский

Если e strictly antitone, то ограниченная карта на s strictly antitone: x < y ⇒ e(x) > e(y).

LaTeX

$$$ x< y \Rightarrow e(x) > e(y) $$$

Lean4

theorem image_strictAnti (hs : StrictAnti e) : StrictAnti (e.image s) :=
  hs.comp_strictMono (Subtype.strictMono_coe _)

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

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

Разделы

Аффилиация

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