pow_lt_top_iff

Mathlib.Algebra.Order.Ring.WithTop

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

English

For x∈WithTop α and n∈ℕ, with Preorder on α, x^n < ⊤ iff x < ⊤ or n = 0.

Русский

Пусть x ∈ WithTop α и n ∈ ℕ; при наличии предиката порядка на α: x^n < ⊤ эквивалентно x < ⊤ или n = 0.

LaTeX

$$$ x^n < \\top \\iff x < \\top \\lor n = 0 $$$

Lean4

@[simp]
theorem pow_lt_top_iff [Preorder α] : x ^ n < ⊤ ↔ x < ⊤ ∨ n = 0 := by
  simp_rw [WithTop.lt_top_iff_ne_top, pow_ne_top_iff]

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

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

Разделы

Аффилиация

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