mul_self_lt_mul_self_iff — Mathlib

English

Let R be PosMulStrictMono and MulPosMono. For 0 ≤ a and 0 ≤ b, 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 < b \iff a * a < b * b)$$$

Lean4

theorem mul_self_lt_mul_self_iff [PosMulStrictMono R] [MulPosMono R] {a b : R} (h1 : 0 ≤ a) (h2 : 0 ≤ b) :
    a < b ↔ a * a < b * b :=
  ((@strictMonoOn_mul_self R _).lt_iff_lt h1 h2).symm

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