comapRight_compProd_id_prod — Mathlib

English

A variant of comapRight with prod map along identity yields κ ⊗ (comapRight η hf) where hf is a measurable embedding.

Русский

Вариант ComapRight для prodMap вдоль идентичности, даёт κ ⊗ (comapRight η hf).

LaTeX

$$$$ comapRight (κ ⊗ₖ η) (\\mathrm{MeasurableEmbedding.id.prodMap}\, hf) = κ ⊗ₖ (comapRight η hf). $$$$

Lean4

theorem comapRight_compProd_id_prod {δ : Type*} {mδ : MeasurableSpace δ} (κ : Kernel α β) [IsSFiniteKernel κ]
    (η : Kernel (α × β) γ) [IsSFiniteKernel η] {f : δ → γ} (hf : MeasurableEmbedding f) :
    comapRight (κ ⊗ₖ η) (MeasurableEmbedding.id.prodMap hf) = κ ⊗ₖ (comapRight η hf) :=
  by
  ext a t ht
  rw [comapRight_apply' _ _ _ ht, compProd_apply, compProd_apply ht]
  · refine lintegral_congr fun b ↦ ?_
    rw [comapRight_apply']
    · congr with x
      aesop
    · exact measurable_prodMk_left ht
  · exact (MeasurableEmbedding.id.prodMap hf).measurableSet_image.mpr ht

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