mul_self_le_mul_self_iff — Mathlib

English

Let R be a PosMulStrictMono and MulPosMono. For 0 ≤ a and 0 ≤ b, we have a ≤ b iff a^2 ≤ b^2.

Русский

Пусть R удовлетворяет PosMulStrictMono и MulPosMono. При 0 ≤ a и 0 ≤ b имеем a ≤ b, тогда a^2 ≤ b^2 и наоборот.

LaTeX

$$$0 \le a \land 0 \le b \Rightarrow (a \le b \iff a * a \le b * b)$$$

Lean4

theorem mul_self_le_mul_self_iff [PosMulStrictMono R] [MulPosMono R] {a b : R} (h1 : 0 ≤ a) (h2 : 0 ≤ b) :
    a ≤ b ↔ a * a ≤ b * b :=
  ⟨mul_self_le_mul_self h1, nonneg_le_nonneg_of_sq_le_sq h2⟩

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