iterate — Mathlib

English

From a quasi-preserving map, the function is a.e.-measurable with respect to the domain measure.

Русский

Из квази-сохраняющей карты следует, что функция является а.е.-измеримой относительно меры области.

LaTeX

$$QuasiMeasurePreserving aemeasurable$$

Lean4

protected theorem iterate {f : α → α} (hf : QuasiMeasurePreserving f μa μa) : ∀ n, QuasiMeasurePreserving f^[n] μa μa
  | 0 => QuasiMeasurePreserving.id μa
  | n + 1 => (hf.iterate n).comp hf

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