le_iff_ge

Mathlib.Order.Monotone.Basic

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

English

If f is strictly anti-on a set s, then f a ≤ f b is equivalent to b ≤ a for a,b ∈ s.

Русский

Если f на множестве s строго антимонотонна, то f(a) ≤ f(b) эквивалентно b ≤ a для a,b ∈ s.

LaTeX

$$$hf.dual_right.le_iff_le hb ha$$$

Lean4

theorem le_iff_ge (hf : StrictAntiOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : f a ≤ f b ↔ b ≤ a :=
  hf.dual_right.le_iff_le hb ha

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

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

Разделы

Аффилиация

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