coe_pow

Mathlib.Algebra.Order.Interval.Set.Instances

URI: https://scilib.ai/kg/mathlib#Set.Ioc.coe_pow

English

The embedding preserves powers.

Русский

Приведение сохраняет возведение в степень.

LaTeX

$$$\uparrow (x^n) = (\uparrow x)^n$$$

Lean4

@[simp, norm_cast]
theorem coe_pow (x : Ioc (0 : R) 1) (n : ℕ) : ↑(x ^ n) = ((x : R) ^ n) :=
  rfl

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

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

Разделы

Аффилиация

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