comp_congr

Mathlib.Probability.Kernel.Composition.MeasureComp

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.comp_congr

English

If κ and η agree almost everywhere with respect to μ, then κ ∘ₘ μ equals η ∘ₘ μ.

Русский

Если κ и η совпадают почти всюду по μ, то κ ∘ₘ μ = η ∘ₘ μ.

LaTeX

$$κ ∘ₘ μ = η ∘ₘ μ$$

Lean4

theorem comp_congr (h : ∀ᵐ a ∂μ, κ a = η a) : κ ∘ₘ μ = η ∘ₘ μ :=
  bind_congr_right h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru