nonneg_le_nonneg_of_sq_le_sq — Mathlib

English

Let R be PosMulStrictMono and MulPosMono. If 0 ≤ b and a² ≤ b², then a ≤ b.

Русский

Пусть R удовлетворяет PosMulStrictMono и MulPosMono. Если 0 ≤ b и a² ≤ b², то a ≤ b.

LaTeX

$$$0 \le b \land a * a \le b * b \Rightarrow a \le b$$$

Lean4

theorem nonneg_le_nonneg_of_sq_le_sq [PosMulStrictMono R] [MulPosMono R] {a b : R} (hb : 0 ≤ b) (h : a * a ≤ b * b) :
    a ≤ b :=
  le_of_not_gt fun hab => (mul_self_lt_mul_self hb hab).not_ge h

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