lt_iff_gt

Mathlib.Order.Monotone.Basic

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

English

On a set, a < b is equivalent to f(a) > f(b) for a strictly anti-on function.

Русский

На множестве a < b эквивалентно f(a) > f(b) для строго антимонотонной f.

LaTeX

$$$hf : StrictAntiOn f s \\Rightarrow ∀ {a b}, a ∈ s → b ∈ s → f a < f b ↔ b < a$$$

Lean4

theorem lt_iff_gt (hf : StrictAntiOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : f a < f b ↔ b < a :=
  hf.dual_right.lt_iff_lt hb ha

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

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

Разделы

Аффилиация

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