pow — Mathlib

English

The n-th power of a strongly measurable function is strongly measurable.

Русский

Степень n-й степени сильно измеримой функции является сильно измеримой.

LaTeX

$$$\text{StronglyMeasurable}(f) \Rightarrow \forall n\in\mathbb{N},\ \text{StronglyMeasurable}(f^n)$$$

Lean4

@[to_additive (attr := fun_prop, aesop safe 20 apply (rule_sets := [Measurable])) const_nsmul]
protected theorem pow [Monoid β] [ContinuousMul β] (hf : StronglyMeasurable f) (n : ℕ) : StronglyMeasurable (f ^ n) :=
  ⟨fun k => hf.approx k ^ n, fun x => (hf.tendsto_approx x).pow n⟩

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