inv_antitoneOn_Iio

Mathlib.Algebra.Order.Field.Basic

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

English

The map x ↦ x^{-1} is antitone on (−∞, 0).

Русский

Функция x ↦ x^{-1} антиотрицательно возрастает на (−∞, 0).

LaTeX

$$$\forall x,y < 0,\ x \le y \implies x^{-1} \ge y^{-1}$$$

Lean4

theorem inv_antitoneOn_Iio : AntitoneOn (fun x : α ↦ x⁻¹) (Set.Iio 0) :=
  by
  convert sub_inv_antitoneOn_Iio (α := α)
  exact (sub_zero _).symm

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

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

Разделы

Аффилиация

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