pow — Mathlib

English

If f: α → β is AEStronglyMeasurable and β is a monoid with continuous multiplication, then f^n is AEStronglyMeasurable for all natural n.

Русский

Если f: α → β является AEStronglyMeasurable и β — моноид с непрерывным умножением, то f^n является AEStronglyMeasurable для всех натуральных n.

LaTeX

$$$AEStronglyMeasurable\ f μ \rightarrow \forall n \in \mathbb{N}, AEStronglyMeasurable\left(f^n\right) μ$$$

Lean4

@[to_additive (attr := fun_prop, aesop safe 20 apply (rule_sets := [Measurable])) const_nsmul]
protected theorem pow [Monoid β] [ContinuousMul β] (hf : AEStronglyMeasurable[m] f μ) (n : ℕ) :
    AEStronglyMeasurable[m] (f ^ n) μ :=
  ⟨hf.mk f ^ n, hf.stronglyMeasurable_mk.pow _, hf.ae_eq_mk.pow_const _⟩

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