pow_lt_pow_left

Mathlib.Algebra.Order.Ring.WithTop

URI: https://scilib.ai/kg/mathlib#WithTop.pow_lt_pow_left

English

If a < b in WithTop α and n ≠ 0, then a^n < b^n.

Русский

Если a < b в WithTop α и n ≠ 0, то a^n < b^n.

LaTeX

$$$\\\\forall a,b \\\\in \\\\mathrm{WithTop} \\\\alpha, a < b \\\\Rightarrow \\\\forall n, n \\\\neq 0 \\\\Rightarrow a^n < b^n$$$

Lean4

@[gcongr]
protected theorem pow_lt_pow_left (hab : a < b) {n : ℕ} (hn : n ≠ 0) : a ^ n < b ^ n :=
  WithTop.pow_right_strictMono hn hab

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

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

Разделы

Аффилиация

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