antitone_le

Mathlib.Order.BoundedOrder.Monotone

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

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 \\\\le x) \\\\Rightarrow (y \\\\le x)$$$

Lean4

theorem antitone_le {x : α} : Antitone (· ≤ x) := fun _ _ h' h => h'.trans h

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

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

Разделы

Аффилиация

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