English
The comap of a product is the supremum of the comaps. Equivalently, pulling back the product σ-algebra along the map ω ↦ (X ω, Y ω) is the supremum of the pullbacks of the individual σ-algebras.
Русский
Обратное образующее произведения равно наибольшему сверху от обратных образующих каждого фактора; то есть восстанавливая σ-алгебру по карте ω ↦ (Xω, Yω) получаем объединение обратных образующих по X и по Y.
LaTeX
$$$(m_β \otimes m_γ).comap (\lambda ω, (X \omega, Y \omega)) = m_β.comap X \;⊔\; m_γ.comap Y$$$
Lean4
/-- The comap of a product is the supremum of the comaps. -/
theorem comap_prodMk {α β γ : Type*} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (X : α → β) (Y : α → γ) :
(mβ.prod mγ).comap (fun ω ↦ (X ω, Y ω)) = mβ.comap X ⊔ mγ.comap Y :=
by
simp_rw [MeasurableSpace.prod, comap_sup, comap_comp]
rfl
