zpow_lt_one_of_neg₀

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#zpow_lt_one_of_neg₀

English

If 1 < a and n < 0, then a^n < 1.

Русский

Если 1 < a и n < 0, то a^n < 1.

LaTeX

$$$1 < a \land n < 0 \implies a^{n} < 1$$$

Lean4

theorem zpow_lt_one_of_neg₀ (ha : 1 < a) (hn : n < 0) : a ^ n < 1 := by simpa using zpow_right_strictMono₀ ha hn

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

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

Разделы

Аффилиация

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