epow_top

Mathlib.Data.ENat.Pow

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

English

If x > 1, then x^⊤ = ⊤.

Русский

Если x > 1, то x^⊤ = ⊤.

LaTeX

$$$ \forall x \in \mathbb{N}_\infty,\; (1 < x) \Rightarrow x^{\top} = \top.$$$

Lean4

theorem epow_top (h : 1 < x) : x ^ (⊤ : ℕ∞) = ⊤ := by
  simp only [instHPow, instPow, (zero_le_one.trans_lt h).ne.symm, ↓reduceIte, h.ne.symm]

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

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

Разделы

Аффилиация

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