inv_strictAntiOn

Mathlib.Algebra.Order.Field.Basic

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

English

The map x ↦ x^{-1} is strictly anti-order on (0, ∞).

Русский

Функция x ↦ x^{-1} строго убывает на (0, ∞).

LaTeX

$$$\text{StrictAntiOn}(\lambda x:\alpha, x^{-1}, (0,\infty))$$$

Lean4

theorem inv_strictAntiOn : StrictAntiOn (fun x : α => x⁻¹) (Set.Ioi 0) := fun _ hx _ hy xy => (inv_lt_inv₀ hy hx).2 xy

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

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

Разделы

Аффилиация

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