of_ae_eq — Mathlib

English

Given hf: AEMeasurable f μ, the pair f and (hf.mk f) are identDistrib with μ and μ.

Русский

Дано hf: AEMeasurable f μ, пара f и (hf.mk f) идентично распределены относительно μ и μ.

LaTeX

$$$hf :\ AEMeasurable f μ\ \to\ IdentDistrib f (hf.mk f) μ μ$$$

Lean4

protected theorem of_ae_eq {g : α → γ} (hf : AEMeasurable f μ) (heq : f =ᵐ[μ] g) : IdentDistrib f g μ μ :=
  { aemeasurable_fst := hf
    aemeasurable_snd := hf.congr heq
    map_eq := Measure.map_congr heq }

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