sub_inv_antitoneOn_Ioi — Mathlib

English

For any fixed c, the map x ↦ (x − c)^{-1} is antitone on the 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_Ioi : AntitoneOn (fun x ↦ (x - c)⁻¹) (Set.Ioi c) :=
  antitoneOn_iff_forall_lt.mpr fun _ ha _ hb hab ↦
    inv_le_inv₀ (sub_pos.mpr hb) (sub_pos.mpr ha) |>.mpr <| sub_le_sub (le_of_lt hab) le_rfl

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