lt_of_pow_lt_pow_left'

Mathlib.Algebra.Order.Monoid.Unbundled.Pow

URI: https://scilib.ai/kg/mathlib#lt_of_pow_lt_pow_left'

English

Under left- and right-strict monotonicity, if a^n < b^n then a < b.

Русский

При наличии левой и правой строгой монотонности, если a^n < b^n, то a < b.

LaTeX

$$$a^n < b^n \Rightarrow a < b$$$

Lean4

@[to_additive lt_of_nsmul_lt_nsmul_right]
theorem lt_of_pow_lt_pow_left' {a b : M} (n : ℕ) : a ^ n < b ^ n → a < b :=
  (pow_left_mono _).reflect_lt

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru