sub_mul_sub_nonpos_iff — Mathlib

English

In a linearly ordered ring with additive order, (x−a)(x−b) ≤ 0 has an equivalent characterization in terms of a ≤ x ≤ b.

Русский

В упорядоченном кольце выражения (x−a)(x−b) ≤ 0 эквивалентны условию a ≤ x ≤ b.

LaTeX

$$$$(x - a)(x - b) \\le 0 \\iff a \\le x \\land x \\le b.$$$$

Lean4

theorem sub_mul_sub_nonpos_iff [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftMono R] (x : R) (h : a ≤ b) :
    (x - a) * (x - b) ≤ 0 ↔ a ≤ x ∧ x ≤ b :=
  by
  rw [mul_nonpos_iff, sub_nonneg, sub_nonneg, sub_nonpos, sub_nonpos, or_iff_left_iff_imp, and_comm]
  exact And.imp h.trans h.trans'

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