coeFn_pow

Mathlib.MeasureTheory.Function.AEEqFun

URI: https://scilib.ai/kg/mathlib#MeasureTheory.AEEqFun.coeFn_pow

English

The coeFn of f^n equals (coeFn f)^n almost everywhere.

Русский

Образ функций-по-коэф ф^n равен (коэф-ф)^n почти всюду.

LaTeX

$$$ \forall f: α \to_{μ} γ,\ (f^n)^{\wedge} = (f^{\wedge})^{n} \ (\ae).$$$

Lean4

theorem coeFn_pow (f : α →ₘ[μ] γ) (n : ℕ) : ⇑(f ^ n) =ᵐ[μ] (⇑f) ^ n :=
  coeFn_comp _ _ _

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

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

Разделы

Аффилиация

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