sub_inv_antitoneOn_Icc_left — Mathlib

English

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

Русский

Если b < c, то отображение 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}$, при условии $b < c$$$

Lean4

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

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