top_epow

Mathlib.Data.ENat.Pow

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

← MathLib Explorer

English

For any y ≠ 0, ⊤^y = ⊤

Русский

Для любого y ≠ 0, ⊤^y = ⊤

LaTeX

$$$ y \neq 0 \rightarrow (⊤)^{y} = ⊤ $$$

Lean4

theorem top_epow (h : y ≠ 0) : (⊤ : ℕ∞) ^ y = ⊤ := by
  induction y with
  | top => exact top_epow_top
  | coe y => rwa [epow_natCast, pow_eq_top_iff, eq_self ⊤, true_and, ← y.cast_ne_zero (R := ℕ∞)]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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