sub_inv_antitoneOn_Icc_right — Mathlib

English

If c < a, then the function x ↦ (x − c)^{-1} is antitone on the closed interval Icc(a, b).

Русский

Если c < a, то функция x ↦ (x − c)^{-1} антонитна на замкнутом отрезке Icc(a, b).

LaTeX

$$$\forall x,y \in [a,b],\ x \le y \implies (x-c)^{-1} \ge (y-c)^{-1}$, при условии $c < a$$$

Lean4

theorem sub_inv_antitoneOn_Icc_right (ha : c < a) : AntitoneOn (fun x ↦ (x - c)⁻¹) (Set.Icc a b) :=
  by
  by_cases hab : a ≤ b
  · exact sub_inv_antitoneOn_Ioi.mono <| (Set.Icc_subset_Ioi_iff hab).mpr ha
  · simp [hab, Set.Subsingleton.antitoneOn]

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