ae_comp_iff — Mathlib

English

For κ and p, the event p holds almost surely under κ ∘ₘ μ iff it holds almost surely under μ with respect to each κ y.

Русский

Для κ и p выполнение события p почти surely под κ ∘ μ эквивалентно выполнению p почти surely по μ относительно каждого κ y.

LaTeX

$$ae_comp_iff hp : (∀ᵐ z ∂(κ ∘ₘ μ), p z) ↔ ∀ᵐ y ∂μ, ∀ᵐ z ∂κ y, p z$$

Lean4

theorem ae_comp_iff {p : β → Prop} (hp : MeasurableSet {z | p z}) : (∀ᵐ z ∂(κ ∘ₘ μ), p z) ↔ ∀ᵐ y ∂μ, ∀ᵐ z ∂κ y, p z :=
  ⟨ae_ae_of_ae_comp, ae_comp_of_ae_ae hp⟩

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