one_le_zpow_of_nonpos₀

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem one_le_zpow_of_nonpos₀ (ha₀ : 0 < a) (ha₁ : a ≤ 1) (hn : n ≤ 0) : 1 ≤ a ^ n := by
  simpa using zpow_right_anti₀ ha₀ ha₁ hn

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

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

Разделы

Аффилиация

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