coe_pow

Mathlib.Topology.ContinuousMap.Bounded.Basic

URI: https://scilib.ai/kg/mathlib#BoundedContinuousFunction.coe_pow

English

The coercion commutes with taking powers: the function-theoretic coe respects exponentiation.

Русский

Коэ согласуется со степенью: коe f сохраняет возведение в степень.

LaTeX

$$$\\operatorname{coe}(f^n) = (\\operatorname{coe}(f))^n$$$

Lean4

@[to_additive]
theorem coe_pow [Monoid R] [BoundedMul R] [ContinuousMul R] (n : ℕ) (f : α →ᵇ R) : ⇑(f ^ n) = (⇑f) ^ n :=
  rfl

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

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

Разделы

Аффилиация

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