comap_prodMap — Mathlib

English

The comap of Prod.map is the product of the comaps. In other words, pulling back along Prod.map X Y yields the product of the individual pullbacks.

Русский

Обратное отображение Prod.map есть произведение обратных отображений; то есть восстанавливая вдоль Prod.map X Y получаем произведение обратных отображений X и Y.

LaTeX

$$$(m_α \otimes m_β).comap (Prod.map X Y) = (m_α.comap X) \;\text{prod}\\(m_β.comap Y)$$$

Lean4

/-- The comap of `Prod.map` is the product of the comaps. -/
theorem comap_prodMap {α β γ δ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (X : γ → α) (Y : δ → β) :
    (mα.prod mβ).comap (Prod.map X Y) = (mα.comap X).prod (mβ.comap Y) :=
  by
  simp_rw [MeasurableSpace.prod, comap_sup, comap_comp]
  rfl

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