prodMap — Mathlib

English

If f and g are quasi-measure-preserving between μ→ν and τ→υ, then Prod.map f g is quasi-measure-preserving from μ×τ to ν×υ.

Русский

Если f и g сохраняют меры, то Prod.map f g сохраняет произведение мер.

LaTeX

$$QuasiMeasurePreserving (Prod.map f g) (μ × τ) (ν × υ)$$

Lean4

@[fun_prop]
protected theorem prodMap {ω : Type*} {mω : MeasurableSpace ω} {υ : Measure ω} [SFinite μ] [SFinite τ] [SFinite υ]
    {f : α → β} {g : γ → ω} (hf : QuasiMeasurePreserving f μ ν) (hg : QuasiMeasurePreserving g τ υ) :
    QuasiMeasurePreserving (Prod.map f g) (μ.prod τ) (ν.prod υ) :=
  by
  refine ⟨by fun_prop, ?_⟩
  rw [← map_prod_map _ _ (by fun_prop) (by fun_prop)]
  exact hf.absolutelyContinuous.prod hg.absolutelyContinuous

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