sub_mul_sub_pos_iff — Mathlib

English

Equivalent reformulations express (x−a)(x−b) ≤ 0 in terms of a ≤ x ≤ b under the same assumptions.

Русский

Эквивалентные формулировки выражают (x−a)(x−b) ≤ 0 через a ≤ x ≤ b.

LaTeX

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

Lean4

theorem sub_mul_sub_pos_iff [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftMono R] (x : R) (h : a ≤ b) :
    0 < (x - a) * (x - b) ↔ x < a ∨ b < x := by
  rw [mul_pos_iff, sub_pos, sub_pos, sub_neg, sub_neg, and_iff_right_of_imp h.trans_lt, and_iff_left_of_imp h.trans_lt',
    or_comm]

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