iterate — Mathlib

English

If f preserves μ→μ, then each iterate f^[n] preserves μ

Русский

Если f сохраняет меру μ в собой же, то каждый квадрат итераций сохраняет μ

LaTeX

$$$\text{MeasurePreserving } f\, μ\, μ \rightarrow \forall n, \text{MeasurePreserving } f^{[n]}\, μ\, μ$$$

Lean4

protected theorem iterate (hf : MeasurePreserving f μ μ) : ∀ n, MeasurePreserving f^[n] μ μ
  | 0 => .id μ
  | n + 1 => (MeasurePreserving.iterate hf n).comp hf

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