pow_lt_top_iff

Mathlib.Data.ENat.Basic

URI: https://scilib.ai/kg/mathlib#ENat.pow_lt_top_iff

English

For a and n, a^n is strictly less than top iff either a is less than top or n = 0.

Русский

Для a и n, a^n < top тогда и только тогда, когда либо a < top, либо n = 0.

LaTeX

$$$$ a^{n} < \\top \\iff a < \\top \\lor n = 0. $$$$

Lean4

@[simp]
theorem pow_lt_top_iff {n : ℕ} : a ^ n < ⊤ ↔ a < ⊤ ∨ n = 0 :=
  WithTop.pow_lt_top_iff

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

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

Разделы

Аффилиация

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