toENNReal_pow

Mathlib.Data.Real.ENatENNReal

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

English

Powers are preserved by the embedding: the image of x^n equals the nth power of the image of x.

Русский

Степени сохраняются: образ x^n равен степению образа x.

LaTeX

$$$\\uparrow (x^n) = (x^n) \\text{ in } \\mathbb{R}_{\\ge 0,\\infty}.$$$

Lean4

@[simp, norm_cast]
theorem toENNReal_pow (x : ℕ∞) (n : ℕ) : (x ^ n : ℕ∞) = (x : ℝ≥0∞) ^ n :=
  RingHom.map_pow toENNRealRingHom x n

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

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

Разделы

Аффилиация

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