bind_congr_right — Mathlib

English

If h is AEMeasurable f m.join then ∀ᵐ μ ∂m, AEMeasurable f μ.

Русский

Если h — AEMeasurable f m.join, то почти наверняка относительно m выполняется AEMeasurable f μ.

LaTeX

$$AEMeasurable.ae_of_join: (h: AEMeasurable f m.join) → ∀ᵐ μ ∂m, AEMeasurable f μ$$

Lean4

theorem bind_congr_right {μ : Measure α} {f g : α → Measure β} (h : f =ᵐ[μ] g) : μ.bind f = μ.bind g :=
  congrArg join <| map_congr h

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