compProd_restrict_left — Mathlib

English

Restricting the left kernel is equivalent to restricting the product to the left-universal product.

Русский

Ограничение левого ядра эквивалентно ограничению произведения до левого универсального произведения.

LaTeX

$$$$ \mathrm{restrict}(κ, hs) ⊗ₖ η = \mathrm{restrict}(κ ⊗ₖ η, (hs \times \mathsf{univ})). $$$$

Lean4

theorem compProd_restrict_left {s : Set β} (hs : MeasurableSet s) :
    Kernel.restrict κ hs ⊗ₖ η = Kernel.restrict (κ ⊗ₖ η) (hs.prod MeasurableSet.univ) :=
  by
  rw [← compProd_restrict hs MeasurableSet.univ]
  congr; exact Kernel.restrict_univ.symm

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