mem_Icc_iff_abs_le — Mathlib

English

For any x,y,z in a linear ordered additive group, |x − y| ≤ z exactly when y lies in the closed interval with left endpoint x − z and right endpoint x + z.

Русский

Для любого x,y,z в линейно упорядоченной аддитивной группе: |x − y| ≤ z тогда и только тогда y принадлежит чёткому интервалу [x − z, x + z].

LaTeX

$$$|x - y| \le z \iff y \in \mathrm{Icc}(x - z, x + z)$$$

Lean4

theorem mem_Icc_iff_abs_le {R : Type*} [AddCommGroup R] [LinearOrder R] [IsOrderedAddMonoid R] {x y z : R} :
    |x - y| ≤ z ↔ y ∈ Icc (x - z) (x + z) :=
  abs_le.trans <| and_comm.trans <| and_congr sub_le_comm neg_le_sub_iff_le_add

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