copy_comp_map — Mathlib

English

If f is AEMeasurable w.r.t μ, then Kernel.copy β ∘ₘ (μ.map f) = μ.map(a ↦ (f a, f a)).

Русский

Если f — AEMeasurable по отношению к μ, то Kernel.copy β ∘ₘ (μ.map f) = μ.map(a ↦ (f a, f a)).

LaTeX

$$$AEMeasurable(f, μ) \\Rightarrow (Kernel.copy \\beta \\circ_{m} (\\mu.map f)) = \\mu.map (\\lambda a. (f a, f a))$$$

Lean4

theorem copy_comp_map {f : α → β} (hf : AEMeasurable f μ) : Kernel.copy β ∘ₘ (μ.map f) = μ.map (fun a ↦ (f a, f a)) :=
  by
  rw [Kernel.copy, deterministic_comp_eq_map, AEMeasurable.map_map_of_aemeasurable (by fun_prop) hf]
  rfl

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