le_iff_ge

Mathlib.Order.Monotone.Basic

URI: https://scilib.ai/kg/mathlib#StrictAnti.le_iff_ge

English

For a strictly anti-monotone f, f a ≤ f b is equivalent to b ≥ a.

Русский

Для строго антимонотонной f, f(a) ≤ f(b) эквивалентно b ≥ a.

LaTeX

$$$(hf : StrictAnti f) \\to ∀ a b, f a ≤ f b \\leftrightarrow b ≥ a$$$

Lean4

theorem le_iff_ge (hf : StrictAnti f) {a b : α} : f a ≤ f b ↔ b ≤ a :=
  (hf.strictAntiOn Set.univ).le_iff_ge trivial trivial

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

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

Разделы

Аффилиация

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