comp — Mathlib

English

If f is quasi-preserving from μa to μa, then for every natural n, the nth iterate f^[n] is quasi-preserving from μa to μa.

Русский

Если f сохраняет μа к μа, то для каждого натурального n единичный шаг итерации f^[n] сохраняет μа к μа.

LaTeX

$$QuasiMeasurePreserving f μa μa → ∀ n, QuasiMeasurePreserving (Nat.iterate f n) μa μa$$

Lean4

@[fun_prop]
protected theorem comp {g : β → γ} {f : α → β} (hg : QuasiMeasurePreserving g μb μc)
    (hf : QuasiMeasurePreserving f μa μb) : QuasiMeasurePreserving (g ∘ f) μa μc :=
  ⟨hg.measurable.comp hf.measurable, by
    rw [← map_map hg.1 hf.1]
    exact (hf.2.map hg.1).trans hg.2⟩

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