ae_compProd_iff — Mathlib

English

A streamlined version of ae_compProd_iff where indicator sets are used to describe p.

Русский

Упрощенная версия ae_compProd_iff, где p выражается через множества-индикаторы.

LaTeX

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

Lean4

theorem ae_compProd_iff {p : β × γ → Prop} (hp : MeasurableSet {x | p x}) :
    (∀ᵐ bc ∂(κ ⊗ₖ η) a, p bc) ↔ ∀ᵐ b ∂κ a, ∀ᵐ c ∂η (a, b), p (b, c) :=
  ⟨fun h ↦ ae_ae_of_ae_compProd h, fun h ↦ ae_compProd_of_ae_ae hp h⟩

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