one_lt_pow'

Mathlib.Algebra.Order.Monoid.Unbundled.Pow

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

English

If a > 1, then a^k > 1 for any k ≠ 0.

Русский

Если a > 1, то a^k > 1 для любого k ≠ 0.

LaTeX

$$$ a > 1 \Rightarrow (k \neq 0 \Rightarrow a^k > 1) $$$

Lean4

@[to_additive nsmul_pos]
theorem one_lt_pow' (ha : 1 < a) {k : ℕ} (hk : k ≠ 0) : 1 < a ^ k :=
  pow_lt_one' (M := Mᵒᵈ) ha hk

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

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

Разделы

Аффилиация

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