comp_compQuasiMeasurePreserving — Mathlib

English

Composition of two AEEqFun compositions preserves quasi-measure-preserving structure.

Русский

Композиция двух AEEquFun сохраняет квазисохранение меры.

LaTeX

$$$(comp g hg f).\\mathrm{compQuasiMeasurePreserving} φ hφ = comp g hg (f.compQuasiMeasurePreserving φ hφ)$$$

Lean4

theorem comp_compQuasiMeasurePreserving {β : Type*} [MeasurableSpace β] {ν} (g : γ → δ) (hg : Continuous g)
    (f : β →ₘ[ν] γ) {φ : α → β} (hφ : Measure.QuasiMeasurePreserving φ μ ν) :
    (comp g hg f).compQuasiMeasurePreserving φ hφ = comp g hg (f.compQuasiMeasurePreserving φ hφ) := by rcases f; rfl

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