sub_inv_antitoneOn_Iio — Mathlib

English

For any fixed c, the map x ↦ (x − c)^{-1} is antitone on the lower open interval (−∞, c).

Русский

Для фиксированного c отображение x ↦ (x − c)^{-1} антонитно на интервале (−∞, c).

LaTeX

$$$\forall x,y < c,\ x \le y \implies (x-c)^{-1} \ge (y-c)^{-1}$$$

Lean4

theorem sub_inv_antitoneOn_Iio : AntitoneOn (fun x ↦ (x - c)⁻¹) (Set.Iio c) :=
  antitoneOn_iff_forall_lt.mpr fun _ ha _ hb hab ↦
    inv_le_inv_of_neg (sub_neg.mpr hb) (sub_neg.mpr ha) |>.mpr <| sub_le_sub (le_of_lt hab) le_rfl

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