ae_ae_of_ae_compProd — Mathlib

English

If almost surely in (a,b) for κ, the property p holds for all (a,b), then a.e. in a, p holds for almost all b and c under η.

Русский

Если почти наверняка по (a,b) для κ выполняется свойство p, то почти наверняка по a свойства p держатся для almost all b и c под η.

LaTeX

$$$$ (∀ᵐ b ∂κ a)(∀ᵐ c ∂η (a,b), p(b,c)) \Rightarrow (∀ᵐ bc ∂(κ ⊗ₖ η) a, p(b,c)). $$$$

Lean4

theorem ae_ae_of_ae_compProd {p : β × γ → Prop} (h : ∀ᵐ bc ∂(κ ⊗ₖ η) a, p bc) : ∀ᵐ b ∂κ a, ∀ᵐ c ∂η (a, b), p (b, c) :=
  ae_null_of_compProd_null h

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