iterate — Mathlib

English

If f is measurable, then all iterates f^[n] are measurable for every n ∈ ℕ.

Русский

Если f измерима, то все иттерации f^[n] измеримы при любом натуральном n.

LaTeX

$$$\\text{Measurable } f \\Rightarrow \\forall n \\in \\mathbb{N},\\ Measurable f^{[n]}$$$

Lean4

@[measurability]
theorem iterate {f : α → α} (hf : Measurable f) : ∀ n, Measurable f^[n]
  | 0 => measurable_id
  | n + 1 => (Measurable.iterate hf n).comp hf

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