pow_lt_pow_iff_left₀ — Mathlib

English

Let a, b be nonnegative elements and n a positive integer. In a linearly ordered monoid with zero, where multiplication by positive elements is strictly increasing, we have a^n < b^n if and only if a < b.

Русский

Пусть a, b неотрицательны и n—положительное целое число. В линейно упорядоченном моноиде с нулём, где умножение на положительное число строго возрастает, выполняется a^n < b^n тогда и только тогда, когда a < b.

LaTeX

$$$\forall a,b\in M_0,\ 0\le a,0\le b,\forall n\in\mathbb{N},\ n\neq 0\Rightarrow a^n < b^n \iff a < b$$$

Lean4

theorem pow_lt_pow_iff_left₀ [MulPosMono M₀] (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : n ≠ 0) : a ^ n < b ^ n ↔ a < b :=
  (pow_left_strictMonoOn₀ hn).lt_iff_lt ha hb

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