strictAnti_of_le_iff_le

Mathlib.Order.Monotone.Defs

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

← MathLib Explorer

English

If x ≤ y iff f y ≤ f x, then f is StrictAnti.

Русский

Если x ≤ y ⇔ f y ≤ f x, то f строго антимонотонна.

LaTeX

$$[Preorder α] [Preorder β] {f : α → β} (h : ∀ x y, x ≤ y ↔ f y ≤ f x) → StrictAnti f$$

Lean4

theorem strictAnti_of_le_iff_le [Preorder α] [Preorder β] {f : α → β} (h : ∀ x y, x ≤ y ↔ f y ≤ f x) : StrictAnti f :=
  fun _ _ ↦ (lt_iff_lt_of_le_iff_le' (h _ _) (h _ _)).1

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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