sub_mul_sub_neg_iff — Mathlib

English

Under the standard assumptions, (x−a)(x−b) < 0 iff a < x < b.

Русский

При существующих предположениях (x−a)(x−b) < 0 эквивалентно a < x < b.

LaTeX

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

Lean4

theorem sub_mul_sub_neg_iff [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftMono R] (x : R) (h : a ≤ b) :
    (x - a) * (x - b) < 0 ↔ a < x ∧ x < b :=
  by
  rw [mul_neg_iff, sub_pos, sub_pos, sub_neg, sub_neg, or_iff_left_iff_imp, and_comm]
  exact And.imp h.trans_lt h.trans_lt'

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