image_antitone

Mathlib.Logic.Equiv.Set

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

English

If e is antitone on α, then for x ≤ y in s we have e(x) ≥ e(y).

Русский

Если e антимонотонна на α, то для x ≤ y в s имеет место e(x) ≥ e(y).

LaTeX

$$$ (\forall x,y\in s) \, x \le y \Rightarrow e(x) \ge e(y) $$$

Lean4

theorem image_antitone (hs : Antitone e) : Antitone (e.image s) :=
  hs.comp_monotone (Subtype.mono_coe _)

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

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

Разделы

Аффилиация

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