dirac_prod_dirac — Mathlib

English

Restricting the first factor to s and keeping the second unrestricted equals restricting the product to s × univ.

Русский

Ограничение первого множителя до s и второго доuniv равно ограничению произведения до s × univ.

LaTeX

$$$\\forall s:\\ Set α,\\; (μ.restrict s).prod ν = (μ.prod ν).restrict (s ×ˢ univ)$$$

Lean4

theorem dirac_prod_dirac {x : α} {y : β} : (dirac x).prod (dirac y) = dirac (x, y) := by
  rw [prod_dirac, map_dirac measurable_prodMk_right]

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