antitone_lt

Mathlib.Order.BoundedOrder.Monotone

URI: https://scilib.ai/kg/mathlib#antitone_lt

English

For a fixed x, the predicate y ↦ y < x is antitone in y: if y ≤ z then z < x implies y < x.

Русский

Для фиксированного x предикат y ↦ y < x антимонотонен по y: если y ≤ z, то z < x ⇒ y < x.

LaTeX

$$$\\\\forall y,z\\\\in \\\\alpha,\\\\ y \\\\le z \\\\Rightarrow (z < x) \\\\Rightarrow (y < x)$$$

Lean4

theorem antitone_lt {x : α} : Antitone (· < x) := fun _ _ h' h => h'.trans_lt h

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

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

Разделы

Аффилиация

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